<!DOCTYPE html>
<html class="client-nojs vector-feature-night-mode-disabled vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-sticky-header-enabled" lang="en" dir="ltr"><head>
<meta charset="UTF-8">
<title>Formal language</title>
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<link rel="canonical" href="https://en.wikipedia.org/wiki/Formal_language"> <link href="./mw/ext.cite.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/ext.math.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.icons.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.search.codex.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/user.styles.css" rel="stylesheet" type="text/css">
<meta name="ResourceLoaderDynamicStyles" content="">
<link rel="stylesheet" type="text/css" href="./mw/site.styles.css">
<link rel="stylesheet" type="text/css" href="./mw/noscript.css">
<link rel="stylesheet" type="text/css" href="./footer.css">
<link rel="stylesheet" type="text/css" href="./vector-2022.css">
</head>
<body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject page-Formal_language rootpage-Formal_language skin-vector-2022 action-view">
<div class="mw-page-container">
<div class="mw-page-container-inner">
<div class="mw-content-container">
<main id="content" class="mw-body">
<header class="mw-body-header vector-page-titlebar">
<h1 id="firstHeading" class="firstHeading mw-first-heading">
<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Formal language</span></span>
</h1>
</header>
<a id="top"></a>
<div id="bodyContent" class="vector-body ve-init-mw-desktopArticleTarget-targetContainer" aria-labelledby="firstHeading" data-mw-ve-target-container="">
<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="en" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr">
<style data-mw-deduplicate="TemplateStyles:r1236090951">
/* start https://en.wikipedia.org/ */
.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}
/* end https://en.wikipedia.org/ */
</style><div role="note" class="hatnote navigation-not-searchable">This article is about a technical term in mathematics and computer science. For any formal type of language usage, see <a href="Literary_language" title="Literary language">Literary language</a>. For studies about natural languages, see <a href="Formal_semantics_(natural_language)" title="Formal semantics (natural language)">Formal semantics (natural language)</a>.</div>
<style data-mw-deduplicate="TemplateStyles:r1305433154">
/* start https://en.wikipedia.org/ */
.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}
/* end https://en.wikipedia.org/ */
</style>
<style data-mw-deduplicate="TemplateStyles:r1129693374">
/* start https://en.wikipedia.org/ */
.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}
/* end https://en.wikipedia.org/ */
</style><style data-mw-deduplicate="TemplateStyles:r1246091330">
/* start https://en.wikipedia.org/ */
.mw-parser-output .sidebar{width:22em;float:right;clear:right;margin:0.5em 0 1em 1em;background:var(--background-color-neutral-subtle,#f8f9fa);border:1px solid var(--border-color-base,#a2a9b1);padding:0.2em;text-align:center;line-height:1.4em;font-size:88%;border-collapse:collapse;display:table}body.skin-minerva .mw-parser-output .sidebar{display:table!important;float:right!important;margin:0.5em 0 1em 1em!important}.mw-parser-output .sidebar-subgroup{width:100%;margin:0;border-spacing:0}.mw-parser-output .sidebar-left{float:left;clear:left;margin:0.5em 1em 1em 0}.mw-parser-output .sidebar-none{float:none;clear:both;margin:0.5em 1em 1em 0}.mw-parser-output .sidebar-outer-title{padding:0 0.4em 0.2em;font-size:125%;line-height:1.2em;font-weight:bold}.mw-parser-output .sidebar-top-image{padding:0.4em}.mw-parser-output .sidebar-top-caption,.mw-parser-output .sidebar-pretitle-with-top-image,.mw-parser-output .sidebar-caption{padding:0.2em 0.4em 0;line-height:1.2em}.mw-parser-output .sidebar-pretitle{padding:0.4em 0.4em 0;line-height:1.2em}.mw-parser-output .sidebar-title,.mw-parser-output .sidebar-title-with-pretitle{padding:0.2em 0.8em;font-size:145%;line-height:1.2em}.mw-parser-output .sidebar-title-with-pretitle{padding:0.1em 0.4em}.mw-parser-output .sidebar-image{padding:0.2em 0.4em 0.4em}.mw-parser-output .sidebar-heading{padding:0.1em 0.4em}.mw-parser-output .sidebar-content{padding:0 0.5em 0.4em}.mw-parser-output .sidebar-content-with-subgroup{padding:0.1em 0.4em 0.2em}.mw-parser-output .sidebar-above,.mw-parser-output .sidebar-below{padding:0.3em 0.8em;font-weight:bold}.mw-parser-output .sidebar-collapse .sidebar-above,.mw-parser-output .sidebar-collapse .sidebar-below{border-top:1px solid #aaa;border-bottom:1px solid #aaa}.mw-parser-output .sidebar-navbar{text-align:right;font-size:115%;padding:0 0.4em 0.4em}.mw-parser-output .sidebar-list-title{padding:0 0.4em;text-align:left;font-weight:bold;line-height:1.6em;font-size:105%}.mw-parser-output .sidebar-list-title-c{padding:0 0.4em;text-align:center;margin:0 3.3em}@media(max-width:640px){body.mediawiki .mw-parser-output .sidebar{width:100%!important;clear:both;float:none!important;margin-left:0!important;margin-right:0!important}}body.skin--responsive .mw-parser-output .sidebar a>img{max-width:none!important}@media screen{html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-list-title,html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle{background:transparent!important}html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle a{color:var(--color-progressive)!important}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-list-title,html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle{background:transparent!important}html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle a{color:var(--color-progressive)!important}}@media print{body.ns-0 .mw-parser-output .sidebar{display:none!important}}
/* end https://en.wikipedia.org/ */
</style><table class="sidebar sidebar-collapse nomobile nowraplinks hlist"><tbody><tr><td class="sidebar-pretitle">Part of <i>a series</i> on</td></tr><tr><th class="sidebar-title-with-pretitle"><a href="Formal_languages" class="mw-redirect" title="Formal languages">Formal languages</a></th></tr><tr><td class="sidebar-content" style="padding-top:0.2em;">
<div class="sidebar-list mw-collapsible"><div class="sidebar-list-title" style="background:#ddddff;text-align:center;;color: var(--color-base)"><div class="sidebar-list-title-c">Key concepts</div></div><div class="sidebar-list-content mw-collapsible-content">
<ul><li><a href="Formal_system" title="Formal system">Formal system</a></li>
<li><a href="Alphabet_(formal_languages)" title="Alphabet (formal languages)">Alphabet</a></li>
<li><a href="Syntax_(logic)" title="Syntax (logic)">Syntax</a></li>
<li><a href="Semantics_of_logic" title="Semantics of logic">Formal semantics</a></li>
<li><a href="Semantics_(computer_science)" title="Semantics (computer science)">Semantics (programming languages)</a></li>
<li><a href="Formal_grammar" title="Formal grammar">Formal grammar</a></li>
<li><a href="Formation_rule" title="Formation rule">Formation rule</a></li>
<li><a href="Well-formed_formula" title="Well-formed formula">Well-formed formula</a></li>
<li><a href="Automata_theory" title="Automata theory">Automata theory</a></li>
<li><a href="Regular_expression" title="Regular expression">Regular expression</a></li>
<li><a href="Production_(computer_science)" title="Production (computer science)">Production</a></li>
<li><a href="Ground_expression" title="Ground expression">Ground expression</a></li>
<li><a href="Atomic_formula" title="Atomic formula">Atomic formula</a></li></ul></div></div></td>
</tr><tr><td class="sidebar-content" style="padding-top:0.2em;">
<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="background:#ddddff;text-align:center;;color: var(--color-base)"><div class="sidebar-list-title-c">Applications</div></div><div class="sidebar-list-content mw-collapsible-content">
<ul><li><a href="Formal_methods" title="Formal methods">Formal methods</a></li>
<li><a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">Propositional calculus</a></li>
<li><a href="Predicate_logic" class="mw-redirect" title="Predicate logic">Predicate logic</a></li>
<li><a href="Mathematical_notation" title="Mathematical notation">Mathematical notation</a></li>
<li><a href="Natural_language_processing" title="Natural language processing">Natural language processing</a></li>
<li><a href="Programming_language_theory" title="Programming language theory">Programming language theory</a></li>
<li><a href="Mathematical_linguistics" title="Mathematical linguistics">Mathematical linguistics</a></li>
<li><a href="Computational_linguistics" title="Computational linguistics">Computational linguistics</a></li>
<li><a href="Syntax_analysis" class="mw-redirect" title="Syntax analysis">Syntax analysis</a></li>
<li><a href="Formal_verification" title="Formal verification">Formal verification</a></li>
<li><a href="Automated_theorem_proving" title="Automated theorem proving">Automated theorem proving</a></li></ul></div></div></td>
</tr><tr><td class="sidebar-navbar"><style data-mw-deduplicate="TemplateStyles:r1239400231">
/* start https://en.wikipedia.org/ */
.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}
/* end https://en.wikipedia.org/ */
</style></td></tr></tbody></table>
<p class="mw-empty-elt">
</p>
<p>In <a href="Logic" title="Logic">logic</a>, <a href="Mathematics" title="Mathematics">mathematics</a>, <a href="Computer_science" title="Computer science">computer science</a>, and <a href="Linguistics" title="Linguistics">linguistics</a>, a <b>formal language</b> is a set of <a href="String_(computer_science)" title="String (computer science)">strings</a> whose symbols are taken from a set called "<a href="#Definition">alphabet</a>".
</p><p>The alphabet of a formal language consists of symbols that <a href="Concatenation" title="Concatenation">concatenate</a> into strings (also called "words").<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> Words that belong to a particular formal language are sometimes called <a class="mw-selflink-fragment" href="#Definition"><i>well-formed words</i></a>. A formal language is often defined by means of a <a href="Formal_grammar" title="Formal grammar">formal grammar</a> such as a <a href="Regular_grammar" title="Regular grammar">regular grammar</a> or <a href="Context-free_grammar" title="Context-free grammar">context-free grammar</a>.
</p><p>In computer science, formal languages are used, among others, as the basis for defining the grammar of <a href="Programming_language" title="Programming language">programming languages</a> and formalized versions of subsets of natural languages, in which the words of the language represent concepts that are associated with meanings or <a href="Semantics" title="Semantics">semantics</a>. In <a href="Computational_complexity_theory" title="Computational complexity theory">computational complexity theory</a>, <a href="Decision_problem" title="Decision problem">decision problems</a> are typically defined as formal languages, and <a href="Complexity_class" title="Complexity class">complexity classes</a> are defined as the sets of the formal languages that can be <a href="Parsing" title="Parsing">parsed by machines</a> with limited computational power. In <a href="Logic" title="Logic">logic</a> and the <a href="Foundations_of_mathematics" title="Foundations of mathematics">foundations of mathematics</a>, formal languages are used to represent the syntax of <a href="Axiomatic_system" title="Axiomatic system">axiomatic systems</a>, and <a href="Formalism_(philosophy_of_mathematics)" title="Formalism (philosophy of mathematics)">mathematical formalism</a> is the philosophy that all of mathematics can be reduced to the syntactic manipulation of formal languages in this way.
</p><p>The field of <b>formal language theory</b> studies primarily the purely <a href="Syntactic" class="mw-redirect" title="Syntactic">syntactic</a> aspects of such languages—that is, their internal structural patterns. Formal language theory sprang out of linguistics, as a way of understanding the syntactic regularities of <a href="Natural_language" title="Natural language">natural languages</a>.
</p>
<meta property="mw:PageProp/toc">
<div class="mw-heading mw-heading2"><h2 id="History">History</h2></div>
<p>In the 17th century, <a href="Gottfried_Leibniz" class="mw-redirect" title="Gottfried Leibniz">Gottfried Leibniz</a> imagined and described the <a href="Characteristica_universalis" title="Characteristica universalis">characteristica universalis</a>, a universal and formal language which utilised <a href="Pictographs" class="mw-redirect" title="Pictographs">pictographs</a>. Later, <a href="Carl_Friedrich_Gauss" title="Carl Friedrich Gauss">Carl Friedrich Gauss</a> investigated the problem of <a href="Gauss_notation" title="Gauss notation">Gauss codes</a>.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup>
</p><p><a href="Gottlob_Frege" title="Gottlob Frege">Gottlob Frege</a> attempted to realize Leibniz's ideas, through a notational system first outlined in <i><a href="Begriffsschrift" title="Begriffsschrift">Begriffsschrift</a></i> (1879) and more fully developed in his 2-volume Grundgesetze der Arithmetik (1893/1903).<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> This described a "formal language of pure language."<sup id="cite_ref-Herken1279_4-0" class="reference"><a href="#cite_note-Herken1279-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup>
</p><p>In the first half of the 20th century, several developments were made with relevance to formal languages. <a href="Axel_Thue" title="Axel Thue">Axel Thue</a> published four papers relating to words and language between 1906 and 1914. The last of these introduced what <a href="Emil_Post" class="mw-redirect" title="Emil Post">Emil Post</a> later termed 'Thue Systems', and gave an early example of an <a href="Undecidable_problem" title="Undecidable problem">undecidable problem</a>.<sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup> Post would later use this paper as the basis for a 1947 proof "that the word problem for semigroups was recursively insoluble",<sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup> and later devised the <a href="Post_canonical_system" title="Post canonical system">canonical system</a> for the creation of formal languages.
</p><p>In 1907, <a href="Leonardo_Torres_Quevedo" title="Leonardo Torres Quevedo">Leonardo Torres Quevedo</a> introduced a formal language for the description of mechanical drawings (mechanical devices), in <a href="Vienna" title="Vienna">Vienna</a>. He published "Sobre un sistema de notaciones y símbolos destinados a facilitar la descripción de las máquinas" ("On a system of notations and symbols intended to facilitate the description of machines").<sup id="cite_ref-7" class="reference"><a href="#cite_note-7"><span class="cite-bracket">[</span>7<span class="cite-bracket">]</span></a></sup> <a href="Heinz_Zemanek" title="Heinz Zemanek">Heinz Zemanek</a> rated it as an equivalent to a <a href="Programming_language" title="Programming language">programming language</a> for the numerical control of machine tools.<sup id="cite_ref-Bruderer_8-0" class="reference"><a href="#cite_note-Bruderer-8"><span class="cite-bracket">[</span>8<span class="cite-bracket">]</span></a></sup>
</p><p><a href="Noam_Chomsky" title="Noam Chomsky">Noam Chomsky</a> devised an abstract representation of formal and natural languages, known as the <a href="Chomsky_hierarchy" title="Chomsky hierarchy">Chomsky hierarchy</a>.<sup id="cite_ref-9" class="reference"><a href="#cite_note-9"><span class="cite-bracket">[</span>9<span class="cite-bracket">]</span></a></sup> In 1959 <a href="John_Backus" title="John Backus">John Backus</a> developed the Backus-Naur form to describe the syntax of a high level programming language, following his work in the creation of <a href="FORTRAN" class="mw-redirect" title="FORTRAN">FORTRAN</a>.<sup id="cite_ref-10" class="reference"><a href="#cite_note-10"><span class="cite-bracket">[</span>10<span class="cite-bracket">]</span></a></sup> <a href="Peter_Naur" title="Peter Naur">Peter Naur</a> was the secretary/editor for the ALGOL60 Report in which he used <a href="Backus%E2%80%93Naur_form" title="Backus–Naur form">Backus–Naur form</a> to describe the Formal part of ALGOL60.
</p>
<div class="mw-heading mw-heading2"><h2 id="Words_over_an_alphabet">Words over an alphabet</h2></div>
<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Alphabet_(formal_languages)" title="Alphabet (formal languages)">Alphabet (formal languages)</a></div>
<p>An <i>alphabet</i>, in the context of formal languages, can be any <a href="Set_(mathematics)" title="Set (mathematics)">set</a>; its elements are called <i>letters</i>. An alphabet may contain an <a href="Countable_set" title="Countable set">infinite</a> number of elements;<sup id="cite_ref-11" class="reference"><a href="#cite_note-11"><span class="cite-bracket">[</span>note 1<span class="cite-bracket">]</span></a></sup> however, most definitions in formal language theory specify alphabets with a finite number of elements, and many results apply only to them. It often makes sense to use an <a href="Alphabet" title="Alphabet">alphabet</a> in the usual sense of the word, or more generally any finite <a href="Character_encoding" title="Character encoding">character encoding</a> such as <a href="ASCII" title="ASCII">ASCII</a> or <a href="Unicode" title="Unicode">Unicode</a>.
</p><p>A <b>word</b> over an alphabet can be any finite sequence (i.e., <a href="String_(computer_science)" title="String (computer science)">string</a>) of letters. The set of all words over an alphabet Σ is usually denoted by Σ<sup>*</sup> (using the <a href="Kleene_star" title="Kleene star">Kleene star</a>). The length of a word is the number of letters it is composed of. For any alphabet, there is only one word of length 0, the <i>empty word</i>, which is often denoted by e, ε, λ or even Λ. By concatenation one can combine two words to form a new word, whose length is the sum of the lengths of the original words. The result of concatenating a word with the empty word is the original word.
</p><p>In some applications, especially in <a href="Logic" title="Logic">logic</a>, the alphabet is also known as the <i>vocabulary</i> and words are known as <i>formulas</i> or <i>sentences</i>; this breaks the letter/word metaphor and replaces it by a word/sentence metaphor.
</p>
<div class="mw-heading mw-heading2"><h2 id="Definition">Definition</h2></div>
<p>Given a non-empty set <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">Σ<!-- Σ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>
</semantics>
</math></span><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy"></span>, a <b>formal language <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>L</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L}</annotation>
</semantics>
</math></span><img src="./103168b86f781fe6e9a4a87b8ea1cebe0ad4ede8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle L}" loading="lazy"></span> over <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">Σ<!-- Σ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>
</semantics>
</math></span><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy"></span></b> is a <a href="Subset" title="Subset">subset</a> of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma ^{*}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msup>
<mi mathvariant="normal">Σ<!-- Σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mo>∗<!-- ∗ --></mo>
</mrow>
</msup>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma ^{*}}</annotation>
</semantics>
</math></span><img src="./807344600a40f1de7136f8b54576e12e9428bef4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.732ex; height:2.343ex;" alt="{\displaystyle \Sigma ^{*}}" loading="lazy"></span>, which is the set of <a href="Kleene_star" title="Kleene star">all possible finite-length words over <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">Σ<!-- Σ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>
</semantics>
</math></span><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy"></span></a>. We call the set <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">Σ<!-- Σ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>
</semantics>
</math></span><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy"></span> <a href="Alphabet_(formal_languages)" title="Alphabet (formal languages)"><b>the alphabet of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>L</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L}</annotation>
</semantics>
</math></span><img src="./103168b86f781fe6e9a4a87b8ea1cebe0ad4ede8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle L}" loading="lazy"></span></b></a>. On the other hand, given a formal language <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>L</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L}</annotation>
</semantics>
</math></span><img src="./103168b86f781fe6e9a4a87b8ea1cebe0ad4ede8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle L}" loading="lazy"></span> over <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">Σ<!-- Σ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>
</semantics>
</math></span><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy"></span>, a word <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle w\in \Sigma ^{*}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<msup>
<mi mathvariant="normal">Σ<!-- Σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mo>∗<!-- ∗ --></mo>
</mrow>
</msup>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle w\in \Sigma ^{*}}</annotation>
</semantics>
</math></span><img src="./8861ae978b1183cafefa37263b531d68ca4df792.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:7.237ex; height:2.343ex;" alt="{\displaystyle w\in \Sigma ^{*}}" loading="lazy"></span> is <i>well-formed</i> if <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle w\in L}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<mi>L</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle w\in L}</annotation>
</semantics>
</math></span><img src="./8bfb7287bf983dc0ca38baed0a2d1e9f9e183042.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.088ex; height:2.176ex;" alt="{\displaystyle w\in L}" loading="lazy"></span>. Similarly, an expression <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle E\subseteq \Sigma ^{*}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>E</mi>
<mo>⊆<!-- ⊆ --></mo>
<msup>
<mi mathvariant="normal">Σ<!-- Σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mo>∗<!-- ∗ --></mo>
</mrow>
</msup>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle E\subseteq \Sigma ^{*}}</annotation>
</semantics>
</math></span><img src="./d1c8af51f9cbe6bb56dfa34b4fbf2813bf01d16a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:7.606ex; height:2.509ex;" alt="{\displaystyle E\subseteq \Sigma ^{*}}" loading="lazy"></span> is <i>well-formed</i> if <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle E\subseteq L}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>E</mi>
<mo>⊆<!-- ⊆ --></mo>
<mi>L</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle E\subseteq L}</annotation>
</semantics>
</math></span><img src="./5dbe0b3dc90d238198bb14fee6416c2c3da569bb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:6.457ex; height:2.343ex;" alt="{\displaystyle E\subseteq L}" loading="lazy"></span>. Sometimes, a formal language <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>L</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L}</annotation>
</semantics>
</math></span><img src="./103168b86f781fe6e9a4a87b8ea1cebe0ad4ede8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle L}" loading="lazy"></span> over <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">Σ<!-- Σ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>
</semantics>
</math></span><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy"></span> has a set of clear rules and constraints for the creation of all possible well-formed words from <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma ^{*}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msup>
<mi mathvariant="normal">Σ<!-- Σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mo>∗<!-- ∗ --></mo>
</mrow>
</msup>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma ^{*}}</annotation>
</semantics>
</math></span><img src="./807344600a40f1de7136f8b54576e12e9428bef4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.732ex; height:2.343ex;" alt="{\displaystyle \Sigma ^{*}}" loading="lazy"></span>.
</p><p>In computer science and mathematics, which do not usually deal with <a href="Natural_language" title="Natural language">natural languages</a>, the adjective "formal" is often omitted as redundant. On the other hand, we can just say "a formal language <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>L</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L}</annotation>
</semantics>
</math></span><img src="./103168b86f781fe6e9a4a87b8ea1cebe0ad4ede8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle L}" loading="lazy"></span>" when its alphabet <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">Σ<!-- Σ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>
</semantics>
</math></span><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy"></span> is clear in the context.
</p><p>While formal language theory usually concerns itself with formal languages that are described by some syntactic rules, the actual definition of the concept "formal language" is only as above: a (possibly infinite) set of finite-length strings composed from a given alphabet, no more and no less. In practice, there are many languages that can be described by rules, such as <a href="Regular_language" title="Regular language">regular languages</a> or <a href="Context-free_language" title="Context-free language">context-free languages</a>. The notion of a <a href="Formal_grammar" title="Formal grammar">formal grammar</a> may be closer to the intuitive concept of a "language", one described by syntactic rules. By an abuse of the definition, a particular formal language is often thought of as being accompanied with a formal grammar that describes it.
</p>
<div class="mw-heading mw-heading2"><h2 id="Examples">Examples</h2></div>
<p>The following rules describe a formal language <span class="texhtml mvar" style="font-style:italic;">L</span> over the alphabet Σ = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, +, =}:
</p>
<ul><li>Every nonempty string that does not contain "+" or "=" and does not start with "0" is in <span class="texhtml mvar" style="font-style:italic;">L</span>.</li>
<li>The string "0" is in <span class="texhtml mvar" style="font-style:italic;">L</span>.</li>
<li>A string containing "=" is in <span class="texhtml mvar" style="font-style:italic;">L</span> if and only if there is exactly one "=", and it separates two valid strings of <span class="texhtml mvar" style="font-style:italic;">L</span>.</li>
<li>A string containing "+" but not "=" is in <span class="texhtml mvar" style="font-style:italic;">L</span> if and only if every "+" in the string separates two valid strings of <span class="texhtml mvar" style="font-style:italic;">L</span>.</li>
<li>No string is in <span class="texhtml mvar" style="font-style:italic;">L</span> other than those implied by the previous rules.</li></ul>
<p>Under these rules, the string "23+4=555" is in <span class="texhtml mvar" style="font-style:italic;">L</span>, but the string "=234=+" is not. This formal language expresses <a href="Natural_number" title="Natural number">natural numbers</a>, well-formed additions, and well-formed addition equalities, but it expresses only what they look like (their <a href="Syntax" title="Syntax">syntax</a>), not what they mean (<a href="Semantics" title="Semantics">semantics</a>). For instance, nowhere in these rules is there any indication that "0" means the number zero, "+" means addition, "23+4=555" is false, etc.
</p>
<div class="mw-heading mw-heading3"><h3 id="Constructions">Constructions</h3></div>
<p>For finite languages, one can explicitly enumerate all well-formed words. For example, we can describe a language <span class="texhtml mvar" style="font-style:italic;">L</span> as just <span class="texhtml mvar" style="font-style:italic;">L</span> = {a, b, ab, cba}. The <a href="Degeneracy_(mathematics)" title="Degeneracy (mathematics)">degenerate</a> case of this construction is the <b>empty language</b>, which contains no words at all (<span class="nounderlines"><span class="texhtml mvar" style="font-style:italic;">L</span> = <a href="%E2%88%85" class="mw-redirect" title="∅">∅</a></span>).
</p><p>However, even over a finite (non-empty) alphabet such as Σ = {a, b} there are an infinite number of finite-length words that can potentially be expressed: "a", "abb", "ababba", "aaababbbbaab", .... Therefore, formal languages are typically infinite, and describing an infinite formal language is not as simple as writing <i>L</i> = {a, b, ab, cba}. Here are some examples of formal languages:
</p>
<ul><li><span class="texhtml mvar" style="font-style:italic;">L</span> = Σ<sup>*</sup>, the set of <i>all</i> words over Σ;</li>
<li><span class="texhtml mvar" style="font-style:italic;">L</span> = {a}<sup>*</sup> = {a<sup><i>n</i></sup>}, where <i>n</i> ranges over the natural numbers and "a<sup><i>n</i></sup>" means "a" repeated <i>n</i> times (this is the set of words consisting only of the symbol "a");</li>
<li>the set of syntactically correct programs in a given programming language (the syntax of which is usually defined by a <a href="Context-free_grammar" title="Context-free grammar">context-free grammar</a>);</li>
<li>the set of inputs upon which a certain <a href="Turing_machine" title="Turing machine">Turing machine</a> halts; or</li>
<li>the set of maximal strings of <a href="Alphanumeric" class="mw-redirect" title="Alphanumeric">alphanumeric</a> <a href="ASCII" title="ASCII">ASCII</a> characters on this line, i.e.,<br> the set {the, set, of, maximal, strings, alphanumeric, ASCII, characters, on, this, line, i, e}.</li></ul>
<div class="mw-heading mw-heading2"><h2 id="Language-specification_formalisms">Language-specification formalisms</h2></div>
<p>Formal languages are used as tools in multiple disciplines. However, formal language theory rarely concerns itself with particular languages (except as examples), but is mainly concerned with the study of various types of formalisms to describe languages. For instance, a language can be given as
</p>
<ul><li>those strings generated by some <a href="Formal_grammar" title="Formal grammar">formal grammar</a>;</li>
<li>those strings described or matched by a particular <a href="Regular_expression" title="Regular expression">regular expression</a>;</li>
<li>those strings accepted by some <a href="Automata_theory" title="Automata theory">automaton</a>, such as a <a href="Turing_machine" title="Turing machine">Turing machine</a> or <a href="Finite-state_automaton" class="mw-redirect" title="Finite-state automaton">finite-state automaton</a>;</li>
<li>those strings for which some <a href="Decision_procedure" class="mw-redirect" title="Decision procedure">decision procedure</a> (an <a href="Algorithm" title="Algorithm">algorithm</a> that asks a sequence of related YES/NO questions) produces the answer YES.</li></ul>
<p>Typical questions asked about such formalisms include:
</p>
<ul><li>What is their expressive power? (Can formalism <i>X</i> describe every language that formalism <i>Y</i> can describe? Can it describe other languages?)</li>
<li>What is their recognizability? (How difficult is it to decide whether a given word belongs to a language described by formalism <i>X</i>?)</li>
<li>What is their comparability? (How difficult is it to decide whether two languages, one described in formalism <i>X</i> and one in formalism <i>Y</i>, or in <i>X</i> again, are actually the same language?).</li></ul>
<p>Surprisingly often, the answer to these decision problems is "it cannot be done at all", or "it is extremely expensive" (with a characterization of how expensive). Therefore, formal language theory is a major application area of <a href="Computability_theory" title="Computability theory">computability theory</a> and <a href="Computational_complexity_theory" title="Computational complexity theory">complexity theory</a>. Formal languages may be classified in the <a href="Chomsky_hierarchy" title="Chomsky hierarchy">Chomsky hierarchy</a> based on the expressive power of their generative grammar as well as the complexity of their recognizing <a href="Automata_theory" title="Automata theory">automaton</a>. <a href="Context-free_grammar" title="Context-free grammar">Context-free grammars</a> and <a href="Regular_grammar" title="Regular grammar">regular grammars</a> provide a good compromise between expressivity and ease of <a href="Parsing" title="Parsing">parsing</a>, and are widely used in practical applications.
</p>
<div class="mw-heading mw-heading2"><h2 id="Operations_on_languages">Operations on languages</h2></div>
<p>Certain operations on languages are common. This includes the standard set operations, such as union, intersection, and complement. Another class of operation is the element-wise application of string operations.
</p><p>Examples: suppose <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}}</annotation>
</semantics>
</math></span><img src="./0e79dc1b001f8b923df475ed14de023cbc456013.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{1}}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{2}}</annotation>
</semantics>
</math></span><img src="./c6a952cfe42c86b7741f55a817da0e251793a358.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{2}}" loading="lazy"></span> are languages over some common alphabet <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">Σ<!-- Σ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>
</semantics>
</math></span><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy"></span>.
</p>
<ul><li>The <i><a href="Concatenation" title="Concatenation">concatenation</a></i> <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}\cdot L_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>⋅<!-- ⋅ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}\cdot L_{2}}</annotation>
</semantics>
</math></span><img src="./9baae23a86e910c2912ff231bfacea2bdfe8fc3d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.953ex; height:2.509ex;" alt="{\displaystyle L_{1}\cdot L_{2}}" loading="lazy"></span> consists of all strings of the form <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle vw}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>v</mi>
<mi>w</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle vw}</annotation>
</semantics>
</math></span><img src="./b8354a09980e3eb2de1a7d376cc69b544c43cced.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.792ex; height:1.676ex;" alt="{\displaystyle vw}" loading="lazy"></span> where <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle v}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>v</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle v}</annotation>
</semantics>
</math></span><img src="./e07b00e7fc0847fbd16391c778d65bc25c452597.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.128ex; height:1.676ex;" alt="{\displaystyle v}" loading="lazy"></span> is a string from <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}}</annotation>
</semantics>
</math></span><img src="./0e79dc1b001f8b923df475ed14de023cbc456013.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{1}}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle w}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>w</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle w}</annotation>
</semantics>
</math></span><img src="./88b1e0c8e1be5ebe69d18a8010676fa42d7961e6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.664ex; height:1.676ex;" alt="{\displaystyle w}" loading="lazy"></span> is a string from <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{2}}</annotation>
</semantics>
</math></span><img src="./c6a952cfe42c86b7741f55a817da0e251793a358.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{2}}" loading="lazy"></span>.</li>
<li>The <i>intersection</i> <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}\cap L_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∩<!-- ∩ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}\cap L_{2}}</annotation>
</semantics>
</math></span><img src="./159185961cf4ee1f5bcd827ae7efa311b81da905.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:7.857ex; height:2.509ex;" alt="{\displaystyle L_{1}\cap L_{2}}" loading="lazy"></span> of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}}</annotation>
</semantics>
</math></span><img src="./0e79dc1b001f8b923df475ed14de023cbc456013.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{1}}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{2}}</annotation>
</semantics>
</math></span><img src="./c6a952cfe42c86b7741f55a817da0e251793a358.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{2}}" loading="lazy"></span> consists of all strings that are contained in both languages</li>
<li>The <i>complement</i> <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg L_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \neg L_{1}}</annotation>
</semantics>
</math></span><img src="./a24db32a3203c2727ee17874884b0534f0c6dbf4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.187ex; height:2.509ex;" alt="{\displaystyle \neg L_{1}}" loading="lazy"></span> of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}}</annotation>
</semantics>
</math></span><img src="./0e79dc1b001f8b923df475ed14de023cbc456013.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{1}}" loading="lazy"></span> with respect to <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">Σ<!-- Σ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>
</semantics>
</math></span><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy"></span> consists of all strings over <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Sigma }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">Σ<!-- Σ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \Sigma }</annotation>
</semantics>
</math></span><img src="./9e1f558f53cda207614abdf90162266c70bc5c1e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.678ex; height:2.176ex;" alt="{\displaystyle \Sigma }" loading="lazy"></span> that are not in <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}}</annotation>
</semantics>
</math></span><img src="./0e79dc1b001f8b923df475ed14de023cbc456013.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{1}}" loading="lazy"></span>.</li>
<li>The <a href="Kleene_star" title="Kleene star">Kleene star</a>: the language consisting of all words that are concatenations of zero or more words in the original language;</li>
<li><i>Reversal</i>:
<ul><li>Let <i>ε</i> be the empty word, then <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \varepsilon ^{R}=\varepsilon }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msup>
<mi>ε<!-- ε --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msup>
<mo>=</mo>
<mi>ε<!-- ε --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \varepsilon ^{R}=\varepsilon }</annotation>
</semantics>
</math></span><img src="./ae758239cc614dcd193d45c4d07f8a48f8cc59ab.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.745ex; height:2.676ex;" alt="{\displaystyle \varepsilon ^{R}=\varepsilon }" loading="lazy"></span>, and</li>
<li>for each non-empty word <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle w=\sigma _{1}\cdots \sigma _{n}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>w</mi>
<mo>=</mo>
<msub>
<mi>σ<!-- σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>⋯<!-- ⋯ --></mo>
<msub>
<mi>σ<!-- σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle w=\sigma _{1}\cdots \sigma _{n}}</annotation>
</semantics>
</math></span><img src="./de7c6b87325c73b53b67bc4e43e3657f8c095998.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:13.187ex; height:2.009ex;" alt="{\displaystyle w=\sigma _{1}\cdots \sigma _{n}}" loading="lazy"></span> (where <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \sigma _{1},\ldots ,\sigma _{n}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>σ<!-- σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>,</mo>
<mo>…<!-- … --></mo>
<mo>,</mo>
<msub>
<mi>σ<!-- σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \sigma _{1},\ldots ,\sigma _{n}}</annotation>
</semantics>
</math></span><img src="./3a4aaee3936fcec2bf906c82a25877fea17f119a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:10.106ex; height:2.009ex;" alt="{\displaystyle \sigma _{1},\ldots ,\sigma _{n}}" loading="lazy"></span>are elements of some alphabet), let <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle w^{R}=\sigma _{n}\cdots \sigma _{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msup>
<mi>w</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msup>
<mo>=</mo>
<msub>
<mi>σ<!-- σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo>⋯<!-- ⋯ --></mo>
<msub>
<mi>σ<!-- σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle w^{R}=\sigma _{n}\cdots \sigma _{1}}</annotation>
</semantics>
</math></span><img src="./0b7dcc7c029f3a3d0970bbf12486cec37c4cc81a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:14.667ex; height:3.009ex;" alt="{\displaystyle w^{R}=\sigma _{n}\cdots \sigma _{1}}" loading="lazy"></span>,</li>
<li>then for a formal language <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>L</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L}</annotation>
</semantics>
</math></span><img src="./103168b86f781fe6e9a4a87b8ea1cebe0ad4ede8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.583ex; height:2.176ex;" alt="{\displaystyle L}" loading="lazy"></span>, <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L^{R}=\{w^{R}\mid w\in L\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msup>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msup>
<mo>=</mo>
<mo fence="false" stretchy="false">{</mo>
<msup>
<mi>w</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msup>
<mo>∣<!-- ∣ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<mi>L</mi>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L^{R}=\{w^{R}\mid w\in L\}}</annotation>
</semantics>
</math></span><img src="./29dc7f79c94b5502cb4de5d615371962e94f5981.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.654ex; height:3.176ex;" alt="{\displaystyle L^{R}=\{w^{R}\mid w\in L\}}" loading="lazy"></span>.</li></ul></li>
<li><a href="String_homomorphism" class="mw-redirect" title="String homomorphism">String homomorphism</a></li></ul>
<p>Such <a href="String_operations" title="String operations">string operations</a> are used to investigate <a href="Closure_(mathematics)" title="Closure (mathematics)">closure properties</a> of classes of languages. A class of languages is closed under a particular operation when the operation, applied to languages in the class, always produces a language in the same class again. For instance, the <a href="Context-free_language" title="Context-free language">context-free languages</a> are known to be closed under union, concatenation, and intersection with <a href="Regular_language" title="Regular language">regular languages</a>, but not closed under intersection or complement. The theory of <a href="Cone_(formal_languages)" title="Cone (formal languages)">trios</a> and <a href="Abstract_family_of_languages" title="Abstract family of languages">abstract families of languages</a> studies the most common closure properties of language families in their own right.<sup id="cite_ref-12" class="reference"><a href="#cite_note-12"><span class="cite-bracket">[</span>11<span class="cite-bracket">]</span></a></sup>
</p>
<dl><dd><table class="wikitable">
<caption align="top">Closure properties of language families (<span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}}</annotation>
</semantics>
</math></span><img src="./0e79dc1b001f8b923df475ed14de023cbc456013.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{1}}" loading="lazy"></span> Op <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{2}}</annotation>
</semantics>
</math></span><img src="./c6a952cfe42c86b7741f55a817da0e251793a358.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{2}}" loading="lazy"></span> where both <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}}</annotation>
</semantics>
</math></span><img src="./0e79dc1b001f8b923df475ed14de023cbc456013.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{1}}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{2}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{2}}</annotation>
</semantics>
</math></span><img src="./c6a952cfe42c86b7741f55a817da0e251793a358.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.637ex; height:2.509ex;" alt="{\displaystyle L_{2}}" loading="lazy"></span> are in the language family given by the column). After Hopcroft and Ullman.
</caption>
<tbody><tr>
<th>Operation
</th>
<th>
</th>
<th><a href="Regular_language" title="Regular language">Regular</a>
</th>
<th><a href="DCFL" class="mw-redirect" title="DCFL">DCFL</a>
</th>
<th><a href="Context_free_language" class="mw-redirect" title="Context free language">CFL</a>
</th>
<th><a href="Indexed_language" title="Indexed language">IND</a>
</th>
<th><a href="Context_sensitive_language" class="mw-redirect" title="Context sensitive language">CSL</a>
</th>
<th><a href="Recursive_language" title="Recursive language">recursive</a>
</th>
<th><a href="Recursively_enumerable_language" title="Recursively enumerable language">RE</a>
</th></tr>
<tr>
<td><a href="Union_(set_theory)" title="Union (set theory)">Union</a>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}\cup L_{2}=\{w\mid w\in L_{1}\lor w\in L_{2}\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∪<!-- ∪ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>=</mo>
<mo fence="false" stretchy="false">{</mo>
<mi>w</mi>
<mo>∣<!-- ∣ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∨<!-- ∨ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}\cup L_{2}=\{w\mid w\in L_{1}\lor w\in L_{2}\}}</annotation>
</semantics>
</math></span><img src="./4d257cd807665a3ad81a557ae56717a18377991b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:33.748ex; height:2.843ex;" alt="{\displaystyle L_{1}\cup L_{2}=\{w\mid w\in L_{1}\lor w\in L_{2}\}}" loading="lazy"></span>
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td></tr>
<tr>
<td><a href="Intersection_(set_theory)" title="Intersection (set theory)">Intersection</a>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}\cap L_{2}=\{w\mid w\in L_{1}\land w\in L_{2}\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∩<!-- ∩ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>=</mo>
<mo fence="false" stretchy="false">{</mo>
<mi>w</mi>
<mo>∣<!-- ∣ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∧<!-- ∧ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}\cap L_{2}=\{w\mid w\in L_{1}\land w\in L_{2}\}}</annotation>
</semantics>
</math></span><img src="./c0b02a5103fede46a77471ee118c1d44773db792.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:33.748ex; height:2.843ex;" alt="{\displaystyle L_{1}\cap L_{2}=\{w\mid w\in L_{1}\land w\in L_{2}\}}" loading="lazy"></span>
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td></tr>
<tr>
<td><a href="Complement_(set_theory)" title="Complement (set theory)">Complement</a>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg L_{1}=\{w\mid w\not \in L_{1}\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>=</mo>
<mo fence="false" stretchy="false">{</mo>
<mi>w</mi>
<mo>∣<!-- ∣ --></mo>
<mi>w</mi>
<mo>∉</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \neg L_{1}=\{w\mid w\not \in L_{1}\}}</annotation>
</semantics>
</math></span><img src="./06e6c82f9cceaad96a49f2498d80742132c8b146.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:20.354ex; height:2.843ex;" alt="{\displaystyle \neg L_{1}=\{w\mid w\not \in L_{1}\}}" loading="lazy"></span>
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td></tr>
<tr>
<td><a href="Concatenation" title="Concatenation">Concatenation</a>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}\cdot L_{2}=\{wz\mid w\in L_{1}\land z\in L_{2}\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>⋅<!-- ⋅ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo>=</mo>
<mo fence="false" stretchy="false">{</mo>
<mi>w</mi>
<mi>z</mi>
<mo>∣<!-- ∣ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∧<!-- ∧ --></mo>
<mi>z</mi>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>2</mn>
</mrow>
</msub>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}\cdot L_{2}=\{wz\mid w\in L_{1}\land z\in L_{2}\}}</annotation>
</semantics>
</math></span><img src="./ce6b5a11ca802fd0abbe846965b1220877682a69.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:33.356ex; height:2.843ex;" alt="{\displaystyle L_{1}\cdot L_{2}=\{wz\mid w\in L_{1}\land z\in L_{2}\}}" loading="lazy"></span>
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td></tr>
<tr>
<td>Kleene star
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L_{1}^{*}=\{\varepsilon \}\cup \{wz\mid w\in L_{1}\land z\in L_{1}^{*}\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msubsup>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
<mrow class="MJX-TeXAtom-ORD">
<mo>∗<!-- ∗ --></mo>
</mrow>
</msubsup>
<mo>=</mo>
<mo fence="false" stretchy="false">{</mo>
<mi>ε<!-- ε --></mi>
<mo fence="false" stretchy="false">}</mo>
<mo>∪<!-- ∪ --></mo>
<mo fence="false" stretchy="false">{</mo>
<mi>w</mi>
<mi>z</mi>
<mo>∣<!-- ∣ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>∧<!-- ∧ --></mo>
<mi>z</mi>
<mo>∈<!-- ∈ --></mo>
<msubsup>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
<mrow class="MJX-TeXAtom-ORD">
<mo>∗<!-- ∗ --></mo>
</mrow>
</msubsup>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L_{1}^{*}=\{\varepsilon \}\cup \{wz\mid w\in L_{1}\land z\in L_{1}^{*}\}}</annotation>
</semantics>
</math></span><img src="./c2011c7ac82efd1d10b1edcd52dd627600ba932b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:35.031ex; height:3.009ex;" alt="{\displaystyle L_{1}^{*}=\{\varepsilon \}\cup \{wz\mid w\in L_{1}\land z\in L_{1}^{*}\}}" loading="lazy"></span>
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td></tr>
<tr>
<td>(String) homomorphism <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>h</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle h}</annotation>
</semantics>
</math></span><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h(L_{1})=\{h(w)\mid w\in L_{1}\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>h</mi>
<mo stretchy="false">(</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>=</mo>
<mo fence="false" stretchy="false">{</mo>
<mi>h</mi>
<mo stretchy="false">(</mo>
<mi>w</mi>
<mo stretchy="false">)</mo>
<mo>∣<!-- ∣ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle h(L_{1})=\{h(w)\mid w\in L_{1}\}}</annotation>
</semantics>
</math></span><img src="./9c76865e5e57da428387eb81fb102b6c6e5e6751.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:25.1ex; height:2.843ex;" alt="{\displaystyle h(L_{1})=\{h(w)\mid w\in L_{1}\}}" loading="lazy"></span>
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td></tr>
<tr>
<td>ε-free (string) homomorphism <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>h</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle h}</annotation>
</semantics>
</math></span><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h(L_{1})=\{h(w)\mid w\in L_{1}\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>h</mi>
<mo stretchy="false">(</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>=</mo>
<mo fence="false" stretchy="false">{</mo>
<mi>h</mi>
<mo stretchy="false">(</mo>
<mi>w</mi>
<mo stretchy="false">)</mo>
<mo>∣<!-- ∣ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle h(L_{1})=\{h(w)\mid w\in L_{1}\}}</annotation>
</semantics>
</math></span><img src="./9c76865e5e57da428387eb81fb102b6c6e5e6751.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:25.1ex; height:2.843ex;" alt="{\displaystyle h(L_{1})=\{h(w)\mid w\in L_{1}\}}" loading="lazy"></span>
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td></tr>
<tr>
<td>Substitution <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \varphi }">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>φ<!-- φ --></mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \varphi }</annotation>
</semantics>
</math></span><img src="./33ee699558d09cf9d653f6351f9fda0b2f4aaa3e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:1.52ex; height:2.176ex;" alt="{\displaystyle \varphi }" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \varphi (L_{1})=\bigcup _{\sigma _{1}\cdots \sigma _{n}\in L_{1}}\varphi (\sigma _{1})\cdot \ldots \cdot \varphi (\sigma _{n})}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>φ<!-- φ --></mi>
<mo stretchy="false">(</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>=</mo>
<munder>
<mo>⋃<!-- ⋃ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<msub>
<mi>σ<!-- σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo>⋯<!-- ⋯ --></mo>
<msub>
<mi>σ<!-- σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mrow>
</munder>
<mi>φ<!-- φ --></mi>
<mo stretchy="false">(</mo>
<msub>
<mi>σ<!-- σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>⋅<!-- ⋅ --></mo>
<mo>…<!-- … --></mo>
<mo>⋅<!-- ⋅ --></mo>
<mi>φ<!-- φ --></mi>
<mo stretchy="false">(</mo>
<msub>
<mi>σ<!-- σ --></mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>n</mi>
</mrow>
</msub>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle \varphi (L_{1})=\bigcup _{\sigma _{1}\cdots \sigma _{n}\in L_{1}}\varphi (\sigma _{1})\cdot \ldots \cdot \varphi (\sigma _{n})}</annotation>
</semantics>
</math></span><img src="./d87d583feb18155c216796a51cd308c247c99a30.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -3.338ex; width:35.766ex; height:5.843ex;" alt="{\displaystyle \varphi (L_{1})=\bigcup _{\sigma _{1}\cdots \sigma _{n}\in L_{1}}\varphi (\sigma _{1})\cdot \ldots \cdot \varphi (\sigma _{n})}" loading="lazy"></span>
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td></tr>
<tr>
<td>Inverse homomorphism <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h^{-1}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msup>
<mi>h</mi>
<mrow class="MJX-TeXAtom-ORD">
<mo>−<!-- − --></mo>
<mn>1</mn>
</mrow>
</msup>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle h^{-1}}</annotation>
</semantics>
</math></span><img src="./8482555dae5cbaa401d8e0cb7d5eb4df203a81b5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.672ex; height:2.676ex;" alt="{\displaystyle h^{-1}}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h^{-1}(L_{1})=\bigcup _{w\in L_{1}}h^{-1}(w)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msup>
<mi>h</mi>
<mrow class="MJX-TeXAtom-ORD">
<mo>−<!-- − --></mo>
<mn>1</mn>
</mrow>
</msup>
<mo stretchy="false">(</mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
<mo stretchy="false">)</mo>
<mo>=</mo>
<munder>
<mo>⋃<!-- ⋃ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<msub>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mn>1</mn>
</mrow>
</msub>
</mrow>
</munder>
<msup>
<mi>h</mi>
<mrow class="MJX-TeXAtom-ORD">
<mo>−<!-- − --></mo>
<mn>1</mn>
</mrow>
</msup>
<mo stretchy="false">(</mo>
<mi>w</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle h^{-1}(L_{1})=\bigcup _{w\in L_{1}}h^{-1}(w)}</annotation>
</semantics>
</math></span><img src="./fa987fc78750adb7034e79cd8186ae7f4ff57cf8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -3.338ex; width:22.973ex; height:5.843ex;" alt="{\displaystyle h^{-1}(L_{1})=\bigcup _{w\in L_{1}}h^{-1}(w)}" loading="lazy"></span>
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td></tr>
<tr>
<td>Reverse
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L^{R}=\{w^{R}\mid w\in L\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<msup>
<mi>L</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msup>
<mo>=</mo>
<mo fence="false" stretchy="false">{</mo>
<msup>
<mi>w</mi>
<mrow class="MJX-TeXAtom-ORD">
<mi>R</mi>
</mrow>
</msup>
<mo>∣<!-- ∣ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<mi>L</mi>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L^{R}=\{w^{R}\mid w\in L\}}</annotation>
</semantics>
</math></span><img src="./29dc7f79c94b5502cb4de5d615371962e94f5981.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.654ex; height:3.176ex;" alt="{\displaystyle L^{R}=\{w^{R}\mid w\in L\}}" loading="lazy"></span>
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#FFC7C7;color:black;vertical-align:middle;text-align:center;" class="table-no">No
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td></tr>
<tr>
<td>Intersection with a <a href="Regular_language" title="Regular language">regular language</a> <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>R</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle R}</annotation>
</semantics>
</math></span><img src="./4b0bfb3769bf24d80e15374dc37b0441e2616e33.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle R}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle L\cap R=\{w\mid w\in L\land w\in R\}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>L</mi>
<mo>∩<!-- ∩ --></mo>
<mi>R</mi>
<mo>=</mo>
<mo fence="false" stretchy="false">{</mo>
<mi>w</mi>
<mo>∣<!-- ∣ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<mi>L</mi>
<mo>∧<!-- ∧ --></mo>
<mi>w</mi>
<mo>∈<!-- ∈ --></mo>
<mi>R</mi>
<mo fence="false" stretchy="false">}</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle L\cap R=\{w\mid w\in L\land w\in R\}}</annotation>
</semantics>
</math></span><img src="./10ca0c16bb1008b9c823a7952891c69eb58b50b1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:29.893ex; height:2.843ex;" alt="{\displaystyle L\cap R=\{w\mid w\in L\land w\in R\}}" loading="lazy"></span>
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td>
<td style="background:#9EFF9E;color:black;vertical-align:middle;text-align:center;" class="table-yes">Yes
</td></tr></tbody></table></dd></dl>
<div class="mw-heading mw-heading2"><h2 id="Applications">Applications</h2></div>
<div class="mw-heading mw-heading3"><h3 id="Programming_languages">Programming languages</h3></div>
<div role="note" class="hatnote navigation-not-searchable">Main articles: <a href="Syntax_(programming_languages)" title="Syntax (programming languages)">Syntax (programming languages)</a> and <a href="Compiler-compiler" title="Compiler-compiler">Compiler-compiler</a></div>
<p>A compiler usually has two distinct components. A <a href="Lexical_analyzer" class="mw-redirect" title="Lexical analyzer">lexical analyzer</a>, sometimes generated by a tool like <a href="Lex_programming_tool" class="mw-redirect" title="Lex programming tool"><code>lex</code></a>, identifies the tokens of the programming language grammar, e.g. <a href="Identifier" title="Identifier">identifiers</a> or <a href="Keyword_(computer_programming)" class="mw-redirect" title="Keyword (computer programming)">keywords</a>, numeric and string literals, punctuation and operator symbols, which are themselves specified by a simpler formal language, usually by means of <a href="Regular_expressions" class="mw-redirect" title="Regular expressions">regular expressions</a>. At the most basic conceptual level, a <a href="Parser" class="mw-redirect" title="Parser">parser</a>, sometimes generated by a <a href="Parser_generator" class="mw-redirect" title="Parser generator">parser generator</a> like <code><a href="Yacc" title="Yacc">yacc</a></code>, attempts to decide if the source program is syntactically valid, that is if it is well formed with respect to the programming language grammar for which the compiler was built.
</p><p>Of course, compilers do more than just parse the source code – they usually translate it into some executable format. Because of this, a parser usually outputs more than a yes/no answer, typically an <a href="Abstract_syntax_tree" title="Abstract syntax tree">abstract syntax tree</a>. This is used by subsequent stages of the compiler to eventually generate an <a href="Executable" title="Executable">executable</a> containing <a href="Machine_code" title="Machine code">machine code</a> that runs directly on the hardware, or some <a href="Intermediate_code" class="mw-redirect" title="Intermediate code">intermediate code</a> that requires a <a href="Virtual_machine" title="Virtual machine">virtual machine</a> to execute.
</p>
<div class="mw-heading mw-heading3"><h3 id="Formal_theories,_systems,_and_proofs">Formal theories, systems, and proofs</h3></div>
<div role="note" class="hatnote navigation-not-searchable">Main articles: <a href="Theory_(mathematical_logic)" title="Theory (mathematical logic)">Theory (mathematical logic)</a> and <a href="Formal_system" title="Formal system">Formal system</a></div>
<p>In <a href="Mathematical_logic" title="Mathematical logic">mathematical logic</a>, a <i>formal theory</i> is a set of <a href="Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">sentences</a> expressed in a formal language.
</p><p>A <i>formal system</i> (also called a <i>logical calculus</i>, or a <i>logical system</i>) consists of a formal language together with a <a href="Deductive_apparatus" class="mw-redirect" title="Deductive apparatus">deductive apparatus</a> (also called a <i>deductive system</i>). The deductive apparatus may consist of a set of <a href="Transformation_rule" class="mw-redirect" title="Transformation rule">transformation rules</a>, which may be interpreted as valid rules of inference, or a set of <a href="Axiom" title="Axiom">axioms</a>, or have both. A formal system is used to <a href="Proof_theory" title="Proof theory">derive</a> one expression from one or more other expressions. Although a formal language can be identified with its formulas, a formal system cannot be likewise identified by its theorems. Two formal systems <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {FS}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mrow class="MJX-TeXAtom-ORD">
<mi class="MJX-tex-caligraphic" mathvariant="script">F</mi>
<mi class="MJX-tex-caligraphic" mathvariant="script">S</mi>
</mrow>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\mathcal {FS}}}</annotation>
</semantics>
</math></span><img src="./ab025245b89b5d8e91a0f027632b0c1764ab2a9f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.419ex; height:2.176ex;" alt="{\displaystyle {\mathcal {FS}}}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {FS'}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mrow class="MJX-TeXAtom-ORD">
<mi class="MJX-tex-caligraphic" mathvariant="script">F</mi>
<msup>
<mi class="MJX-tex-caligraphic" mathvariant="script">S</mi>
<mo>′</mo>
</msup>
</mrow>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\mathcal {FS'}}}</annotation>
</semantics>
</math></span><img src="./23a8dd711a545583eab7b71b7cf80d57ee84344c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.129ex; height:2.509ex;" alt="{\displaystyle {\mathcal {FS'}}}" loading="lazy"></span> may have all the same theorems and yet differ in some significant proof-theoretic way (a formula A may be a syntactic consequence of a formula B in one but not another for instance).
</p><p>A <i>formal proof</i> or <i>derivation</i> is a finite sequence of well-formed formulas (which may be interpreted as sentences, or <a href="Proposition" title="Proposition">propositions</a>) each of which is an axiom or follows from the preceding formulas in the sequence by a <a href="Rule_of_inference" title="Rule of inference">rule of inference</a>. The last sentence in the sequence is a theorem of a formal system. Formal proofs are useful because their theorems can be interpreted as true propositions.
</p>
<div class="mw-heading mw-heading4"><h4 id="Interpretations_and_models">Interpretations and models</h4></div>
<div role="note" class="hatnote navigation-not-searchable">Main articles: <a href="Formal_semantics_(logic)" class="mw-redirect" title="Formal semantics (logic)">Formal semantics (logic)</a>, <a href="Interpretation_(logic)" title="Interpretation (logic)">Interpretation (logic)</a>, and <a href="Model_theory" title="Model theory">Model theory</a></div>
<p>Formal languages are entirely syntactic in nature, but may be given <a href="Semantics" title="Semantics">semantics</a> that give meaning to the elements of the language. For instance, in mathematical <a href="Logic" title="Logic">logic</a>, the set of possible formulas of a particular logic is a formal language, and an <a href="Interpretation_(logic)" title="Interpretation (logic)">interpretation</a> assigns a meaning to each of the formulas—usually, a <a href="Truth_value" title="Truth value">truth value</a>.
</p><p>The study of interpretations of formal languages is called <a href="Formal_semantics_(logic)" class="mw-redirect" title="Formal semantics (logic)">formal semantics</a>. In mathematical logic, this is often done in terms of <a href="Model_theory" title="Model theory">model theory</a>. In model theory, the terms that occur in a formula are interpreted as objects within <a href="Structure_(mathematical_logic)" title="Structure (mathematical logic)">mathematical structures</a>, and fixed compositional interpretation rules determine how the truth value of the formula can be derived from the interpretation of its terms; a <i>model</i> for a formula is an interpretation of terms such that the formula becomes true.
</p>
<div class="mw-heading mw-heading2"><h2 id="See_also">See also</h2></div>
<ul><li><a href="Combinatorics_on_words" title="Combinatorics on words">Combinatorics on words</a></li>
<li><a href="Formal_method" class="mw-redirect" title="Formal method">Formal method</a></li>
<li><a href="Free_monoid" title="Free monoid">Free monoid</a></li>
<li><a href="Grammar_framework" class="mw-redirect" title="Grammar framework">Grammar framework</a></li>
<li><a href="Mathematical_notation" title="Mathematical notation">Mathematical notation</a></li>
<li><a href="String_(computer_science)" title="String (computer science)">String (computer science)</a></li></ul>
<div class="mw-heading mw-heading2"><h2 id="Notes">Notes</h2></div>
<style data-mw-deduplicate="TemplateStyles:r1239543626">
/* start https://en.wikipedia.org/ */
.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}
/* end https://en.wikipedia.org/ */
</style><div class="reflist">
<div class="mw-references-wrap"><ol class="references">
<li id="cite_note-11"><span class="mw-cite-backlink"><b><a href="#cite_ref-11">^</a></b></span> <span class="reference-text">For example, <a href="First-order_logic" title="First-order logic">first-order logic</a> is often expressed using an alphabet that, besides symbols such as ∧, ¬, ∀ and parentheses, contains infinitely many elements <i>x</i><sub>0</sub>, <i>x</i><sub>1</sub>, <i>x</i><sub>2</sub>, … that play the role of variables.</span>
</li>
</ol></div></div>
<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>
<div class="mw-heading mw-heading3"><h3 id="Citations">Citations</h3></div>
<div class="reflist">
<div class="mw-references-wrap mw-references-columns"><ol class="references">
<li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text">See e.g. <style data-mw-deduplicate="TemplateStyles:r1238218222">
/* start https://en.wikipedia.org/ */
.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}
/* end https://en.wikipedia.org/ */
</style><cite id="CITEREFReghizzi2009" class="citation book cs1">Reghizzi, Stefano Crespi (2009). <a rel="nofollow" class="external text" href="https://books.google.com/books?id=AxH6cWm61i0C"><i>Formal Languages and Compilation</i></a>. Texts in Computer Science. Springer. p. 8. <a href="Bibcode_(identifier)" class="mw-redirect" title="Bibcode (identifier)">Bibcode</a>:<a rel="nofollow" class="external text" href="https://ui.adsabs.harvard.edu/abs/2009flc..book.....C">2009flc..book.....C</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9781848820500</bdi>. <q>An alphabet is a finite set</q></cite></span>
</li>
<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://www.researchgate.net/publication/220530857">"In the prehistory of formal language theory: Gauss Languages"</a>. January 1992<span class="reference-accessdate">. Retrieved <span class="nowrap">30 April</span> 2021</span>.</cite></span>
</li>
<li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://plato.stanford.edu/entries/frege/">"Gottlob Frege"</a>. 5 December 2019<span class="reference-accessdate">. Retrieved <span class="nowrap">30 April</span> 2021</span>.</cite></span>
</li>
<li id="cite_note-Herken1279-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-Herken1279_4-0">^</a></b></span> <span class="reference-text"><cite id="CITEREFMartin_Davis1995" class="citation book cs1">Martin Davis (1995). <a rel="nofollow" class="external text" href="https://books.google.com/books?id=YafIDVd1Z68C&pg=PA290">"Influences of Mathematical Logic on Computer Science"</a>. In Rolf Herken (ed.). <i>The universal Turing machine: a half-century survey</i>. Springer. p. 290. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-211-82637-9</bdi>.</cite></span>
</li>
<li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://core.ac.uk/download/pdf/297029993.pdf">"Thue's 1914 paper: a translation"</a> <span class="cs1-format">(PDF)</span>. 28 August 2013. <a rel="nofollow" class="external text" href="https://web.archive.org/web/20210430011129/https://core.ac.uk/download/pdf/297029993.pdf">Archived</a> <span class="cs1-format">(PDF)</span> from the original on 30 April 2021<span class="reference-accessdate">. Retrieved <span class="nowrap">30 April</span> 2021</span>.</cite></span>
</li>
<li id="cite_note-6"><span class="mw-cite-backlink"><b><a href="#cite_ref-6">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://mathshistory.st-andrews.ac.uk/Biographies/Post/">"Emil Leon Post"</a>. September 2001<span class="reference-accessdate">. Retrieved <span class="nowrap">30 April</span> 2021</span>.</cite></span>
</li>
<li id="cite_note-7"><span class="mw-cite-backlink"><b><a href="#cite_ref-7">^</a></b></span> <span class="reference-text">Torres Quevedo, Leonardo. <a rel="nofollow" class="external text" href="https://quickclick.es/rop/pdf/publico/1907/1907_tomoI_1634_01.pdf">Sobre un sistema de notaciones y símbolos destinados a facilitar la descripción de las máquinas, (pdf)</a>, pp. 25–30, Revista de Obras Públicas, 17 January 1907.</span>
</li>
<li id="cite_note-Bruderer-8"><span class="mw-cite-backlink"><b><a href="#cite_ref-Bruderer_8-0">^</a></b></span> <span class="reference-text"><cite id="CITEREFBruderer2021" class="citation book cs1">Bruderer, Herbert (2021). <a rel="nofollow" class="external text" href="https://books.google.com/books?id=Gh8SEAAAQBAJ&dq=leonardo+torres+quevedo+heinz+zemanek+formal+language&pg=PA1212">"The Global Evolution of Computer Technology"</a>. <i>Milestones in Analog and Digital Computing</i>. Springer. p. 1212. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3030409739</bdi>.</cite></span>
</li>
<li id="cite_note-9"><span class="mw-cite-backlink"><b><a href="#cite_ref-9">^</a></b></span> <span class="reference-text"><cite id="CITEREFJagerRogers2012" class="citation journal cs1">Jager, Gerhard; Rogers, James (19 July 2012). <a rel="nofollow" class="external text" href="https://www.ncbi.nlm.nih.gov/pmc/articles/PMC3367686">"Formal language theory: refining the Chomsky hierarchy"</a>. <i>Philosophical Transactions of the Royal Society B</i>. <b>367</b> (1598): <span class="nowrap">1956–</span>1970. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1098%2Frstb.2012.0077">10.1098/rstb.2012.0077</a>. <a href="PMC_(identifier)" class="mw-redirect" title="PMC (identifier)">PMC</a> <span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://www.ncbi.nlm.nih.gov/pmc/articles/PMC3367686">3367686</a></span>. <a href="PMID_(identifier)" class="mw-redirect" title="PMID (identifier)">PMID</a> <a rel="nofollow" class="external text" href="https://pubmed.ncbi.nlm.nih.gov/22688632">22688632</a>.</cite></span>
</li>
<li id="cite_note-10"><span class="mw-cite-backlink"><b><a href="#cite_ref-10">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://mathshistory.st-andrews.ac.uk/Biographies/Backus/">"John Warner Backus"</a>. February 2016<span class="reference-accessdate">. Retrieved <span class="nowrap">30 April</span> 2021</span>.</cite></span>
</li>
<li id="cite_note-12"><span class="mw-cite-backlink"><b><a href="#cite_ref-12">^</a></b></span> <span class="reference-text"><a href="#CITEREFHopcroftUllman1979">Hopcroft & Ullman (1979)</a>, Chapter 11: Closure properties of families of languages.</span>
</li>
</ol></div></div>
<div class="mw-heading mw-heading3"><h3 id="Sources">Sources</h3></div>
<dl><dt>Works cited</dt></dl>
<style data-mw-deduplicate="TemplateStyles:r1239549316">
/* start https://en.wikipedia.org/ */
.mw-parser-output .refbegin{margin-bottom:0.5em}.mw-parser-output .refbegin-hanging-indents>ul{margin-left:0}.mw-parser-output .refbegin-hanging-indents>ul>li{margin-left:0;padding-left:3.2em;text-indent:-3.2em}.mw-parser-output .refbegin-hanging-indents ul,.mw-parser-output .refbegin-hanging-indents ul li{list-style:none}@media(max-width:720px){.mw-parser-output .refbegin-hanging-indents>ul>li{padding-left:1.6em;text-indent:-1.6em}}.mw-parser-output .refbegin-columns{margin-top:0.3em}.mw-parser-output .refbegin-columns ul{margin-top:0}.mw-parser-output .refbegin-columns li{page-break-inside:avoid;break-inside:avoid-column}@media screen{.mw-parser-output .refbegin{font-size:90%}}
/* end https://en.wikipedia.org/ */
</style><div class="refbegin" style="">
<ul><li><cite id="CITEREFHopcroftUllman1979" class="citation book cs1"><a href="John_Hopcroft" title="John Hopcroft">Hopcroft, John E.</a>; <a href="Jeffrey_Ullman" title="Jeffrey Ullman">Ullman, Jeffrey D.</a> (1979). <i><a href="Introduction_to_Automata_Theory%2C_Languages%2C_and_Computation" title="Introduction to Automata Theory, Languages, and Computation">Introduction to Automata Theory, Languages, and Computation</a></i>. Reading, Massachusetts: Addison-Wesley Publishing. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>81-7808-347-7</bdi>.</cite></li></ul>
</div>
<dl><dt>General references</dt></dl>
<div class="refbegin" style="">
<ul><li>A. G. Hamilton, <i>Logic for Mathematicians</i>, <a href="Cambridge_University_Press" title="Cambridge University Press">Cambridge University Press</a>, 1978, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-521-21838-1</bdi>.</li>
<li><a href="Seymour_Ginsburg" title="Seymour Ginsburg">Seymour Ginsburg</a>, <i>Algebraic and automata theoretic properties of formal languages</i>, North-Holland, 1975, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-7204-2506-9</bdi>.</li>
<li><a href="Michael_A._Harrison" title="Michael A. Harrison">Michael A. Harrison</a>, <i>Introduction to Formal Language Theory</i>, Addison-Wesley, 1978.</li>
<li><cite id="CITEREFRautenberg2010" class="citation book cs1"><a href="Wolfgang_Rautenberg" title="Wolfgang Rautenberg">Rautenberg, Wolfgang</a> (2010). <i>A Concise Introduction to Mathematical Logic</i> (3rd ed.). New York: <a href="Springer_Science%2BBusiness_Media" title="Springer Science+Business Media">Springer Science+Business Media</a>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-1-4419-1221-3">10.1007/978-1-4419-1221-3</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-4419-1220-6</bdi>.</cite></li>
<li><a href="Grzegorz_Rozenberg" title="Grzegorz Rozenberg">Grzegorz Rozenberg</a>, <a href="Arto_Salomaa" title="Arto Salomaa">Arto Salomaa</a>, <i>Handbook of Formal Languages: Volume I-III</i>, Springer, 1997, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>3-540-61486-9</bdi>.</li>
<li>Patrick Suppes, <i>Introduction to Logic</i>, D. Van Nostrand, 1957, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-442-08072-7</bdi>.</li></ul>
</div>
<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>
<ul><li><cite class="citation cs2"><a rel="nofollow" class="external text" href="https://www.encyclopediaofmath.org/index.php?title=Formal_language">"Formal language"</a>, <i><a href="Encyclopedia_of_Mathematics" title="Encyclopedia of Mathematics">Encyclopedia of Mathematics</a></i>, <a href="European_Mathematical_Society" title="European Mathematical Society">EMS Press</a>, 2001 [1994]</cite></li>
<li><a href="University_of_Maryland%2C_Baltimore" title="University of Maryland, Baltimore">University of Maryland</a>, <a rel="nofollow" class="external text" href="http://www.csee.umbc.edu/help/theory/lang_def.shtml">Formal Language Definitions</a></li>
<li>James Power, <a rel="nofollow" class="external text" href="http://www.cs.nuim.ie/~jpower/Courses/parsing/">"Notes on Formal Language Theory and Parsing"</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20071121142736/http://www.cs.nuim.ie/~jpower/Courses/parsing/">Archived</a> 21 November 2007 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a>, 29 November 2002.</li>
<li>Drafts of some chapters in the "Handbook of Formal Language Theory", Vol. 1–3, G. Rozenberg and A. Salomaa (eds.), <a href="Springer_Verlag" class="mw-redirect" title="Springer Verlag">Springer Verlag</a>, (1997):
<ul><li>Alexandru Mateescu and Arto Salomaa, <a rel="nofollow" class="external text" href="https://www.cs.cmu.edu/~lkontor/noam/Mateescu-Salomaa.pdf">"Preface" in Vol.1, pp. v–viii, and "Formal Languages: An Introduction and a Synopsis", Chapter 1 in Vol. 1, pp. 1–39</a></li>
<li>Sheng Yu, <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.67.1248&rep=rep1&type=pdf">"Regular Languages", Chapter 2 in Vol. 1</a></li>
<li>Jean-Michel Autebert, Jean Berstel, Luc Boasson, <a rel="nofollow" class="external text" href="https://www-igm.univ-mlv.fr/~berstel/Articles/1997CFLPDA.pdf">"Context-Free Languages and Push-Down Automata", Chapter 3 in Vol. 1</a></li>
<li>Christian Choffrut and Juhani Karhumäki, <a rel="nofollow" class="external text" href="http://www.liafa.jussieu.fr/~cc/PUBLICATIONS/CKTUCS.PS.gz">"Combinatorics of Words", Chapter 6 in Vol. 1</a></li>
<li>Tero Harju and Juhani Karhumäki, <a rel="nofollow" class="external text" href="http://users.utu.fi/harju/articles/morph.pdf">"Morphisms", Chapter 7 in Vol. 1, pp. 439–510</a></li>
<li>Jean-Eric Pin, <a rel="nofollow" class="external text" href="http://www.liafa.jussieu.fr/~jep/PDF/HandBook.pdf">"Syntactic semigroups", Chapter 10 in Vol. 1, pp. 679–746</a></li>
<li>M. Crochemore and C. Hancart, <a rel="nofollow" class="external text" href="http://www-igm.univ-mlv.fr/~mac/REC/DOC/B4.ps">"Automata for matching patterns", Chapter 9 in Vol. 2</a></li>
<li>Dora Giammarresi, Antonio Restivo, <a rel="nofollow" class="external text" href="https://web.archive.org/web/20071008170115/http://bruno.maitresdumonde.com/optinfo/Spe-MP/dmds1998/2dlang/giammaresi-restivo-paper.ps">"Two-dimensional Languages", Chapter 4 in Vol. 3, pp. 215–267</a></li></ul></li></ul>
<div class="navbox-styles"><style data-mw-deduplicate="TemplateStyles:r1126788409">
/* start https://en.wikipedia.org/ */
.mw-parser-output .plainlist ol,.mw-parser-output .plainlist ul{line-height:inherit;list-style:none;margin:0;padding:0}.mw-parser-output .plainlist ol li,.mw-parser-output .plainlist ul li{margin-bottom:0}
/* end https://en.wikipedia.org/ */
</style><style data-mw-deduplicate="TemplateStyles:r1236075235">
/* start https://en.wikipedia.org/ */
.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}
/* end https://en.wikipedia.org/ */
</style></div><div role="navigation" class="navbox" aria-labelledby="Automata_theory:_formal_languages_and_formal_grammars385" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><div id="Automata_theory:_formal_languages_and_formal_grammars385" style="font-size:114%;margin:0 4em"><a href="Automata_theory" title="Automata theory">Automata theory</a>: and <a href="Formal_grammar" title="Formal grammar">formal grammars</a></div></th></tr><tr><td colspan="2" class="navbox-list navbox-odd plainlist" style="width:100%;padding:0;background:transparent;color:inherit;"><div style="padding:0px"><table class="navbox-columns-table" style="border-spacing: 0px; text-align:left;width:100%;"><tbody><tr><td class="navbox-abovebelow" style="font-weight:bold;"><a href="Chomsky_hierarchy" title="Chomsky hierarchy">Chomsky hierarchy</a></td><td class="navbox-abovebelow" style="border-left:2px solid #fdfdfd;font-weight:bold;"><a href="Formal_grammar" title="Formal grammar">Grammars</a></td><td class="navbox-abovebelow" style="border-left:2px solid #fdfdfd;font-weight:bold;"></td><td class="navbox-abovebelow" style="border-left:2px solid #fdfdfd;font-weight:bold;"><a href="Abstract_machine" title="Abstract machine">Abstract machines</a></td></tr><tr style="vertical-align:top"><td class="navbox-list" style="padding:0px;text-align: center;width:10em;"><div>
<ul><li>Type-0</li>
<li>—</li>
<li>Type-1</li>
<li>—</li>
<li>—</li>
<li>—</li>
<li>—</li>
<li>—</li>
<li>Type-2</li>
<li>—</li>
<li>—</li>
<li>Type-3</li>
<li>—</li>
<li>—</li></ul>
</div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;width:10em;"><div>
<ul><li><a href="Unrestricted_grammar" title="Unrestricted grammar">Unrestricted</a></li>
<li>(no common name)</li>
<li><a href="Context-sensitive_grammar" title="Context-sensitive grammar">Context-sensitive</a></li>
<li><span style="white-space:nowrap;">Positive <a href="Range_concatenation_grammars" class="mw-redirect" title="Range concatenation grammars">range concatenation</a></span></li>
<li><a href="Indexed_grammar" title="Indexed grammar">Indexed</a></li>
<li>—</li>
<li><a href="Linear_context-free_rewriting_system" class="mw-redirect" title="Linear context-free rewriting system">Linear context-free rewriting systems</a></li>
<li><a href="Tree-adjoining_grammar" title="Tree-adjoining grammar">Tree-adjoining</a></li>
<li><a href="Context-free_grammar" title="Context-free grammar">Context-free</a></li>
<li><a href="Deterministic_context-free_grammar" title="Deterministic context-free grammar">Deterministic context-free</a></li>
<li><a href="Nested_word" title="Nested word">Visibly pushdown</a></li>
<li><a href="Regular_grammar" title="Regular grammar">Regular</a></li>
<li>—</li>
<li><a href="Non-recursive_grammar" class="mw-redirect" title="Non-recursive grammar">Non-recursive</a></li></ul>
</div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;width:10em;"><div>
<ul><li><a href="Recursively_enumerable_language" title="Recursively enumerable language">Recursively enumerable</a></li>
<li><a href="Recursive_language" title="Recursive language">Decidable</a></li>
<li><a href="Context-sensitive_language" title="Context-sensitive language">Context-sensitive</a></li>
<li><span style="white-space:nowrap;">Positive <a href="Range_concatenation_language" class="mw-redirect" title="Range concatenation language">range concatenation</a><sup>*</sup></span></li>
<li><a href="Indexed_language" title="Indexed language">Indexed</a><sup>*</sup></li>
<li>—</li>
<li><a href="Linear_context-free_rewriting_language" class="mw-redirect" title="Linear context-free rewriting language">Linear context-free rewriting language</a></li>
<li><a href="Tree-adjoining_grammar" title="Tree-adjoining grammar">Tree-adjoining</a></li>
<li><a href="Context-free_language" title="Context-free language">Context-free</a></li>
<li><a href="Deterministic_context-free_language" title="Deterministic context-free language">Deterministic context-free</a></li>
<li><a href="Nested_word" title="Nested word">Visibly pushdown</a></li>
<li><a href="Regular_language" title="Regular language">Regular</a></li>
<li><a href="Star-free_language" title="Star-free language">Star-free</a></li>
<li><a href="Finite_language" class="mw-redirect" title="Finite language">Finite</a></li></ul>
</div></td><td class="navbox-list" style="border-left:2px solid #fdfdfd;padding:0px;width:10em;"><div>
<ul><li><a href="Turing_machine" title="Turing machine">Turing machine</a></li>
<li><a href="Decider_(Turing_machine)" title="Decider (Turing machine)">Decider</a></li>
<li><a href="Linear_bounded_automaton" title="Linear bounded automaton">Linear-bounded</a></li>
<li><a href="PTIME" class="mw-redirect" title="PTIME">PTIME</a> Turing Machine</li>
<li><a href="Nested_stack_automaton" title="Nested stack automaton">Nested stack</a></li>
<li><a href="Thread_automaton" title="Thread automaton">Thread automaton</a></li>
<li>restricted <a href="Tree_stack_automaton" title="Tree stack automaton">Tree stack automaton</a></li>
<li><a href="Embedded_pushdown_automaton" title="Embedded pushdown automaton">Embedded pushdown</a></li>
<li><a href="Pushdown_automaton" title="Pushdown automaton">Nondeterministic pushdown</a></li>
<li><a href="Deterministic_pushdown_automaton" title="Deterministic pushdown automaton">Deterministic pushdown</a></li>
<li><a href="Nested_word" title="Nested word">Visibly pushdown</a></li>
<li><a href="Finite-state_machine" title="Finite-state machine">Finite</a></li>
<li><a href="Aperiodic_finite_state_automaton" class="mw-redirect" title="Aperiodic finite state automaton">Counter-free (with aperiodic finite monoid)</a></li>
<li><a href="Deterministic_acyclic_finite_state_automaton" title="Deterministic acyclic finite state automaton">Acyclic finite</a></li></ul>
</div></td></tr></tbody></table></div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><span style="white-space:nowrap;">Each category of languages, except those marked by a <sup>*</sup>, is a <a href="Proper_subset" class="mw-redirect" title="Proper subset">proper subset</a> of the category directly above it.</span> <span style="white-space:nowrap;">Any language in each category is generated by a grammar and by an automaton in the category in the same line.</span></div></td></tr></tbody></table></div>
<div class="navbox-styles"></div><div role="navigation" class="navbox" aria-labelledby="Mathematical_logic344" style="padding:3px"><table class="nowraplinks mw-collapsible mw-collapsed navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><div id="Mathematical_logic344" style="font-size:114%;margin:0 4em"><a href="Mathematical_logic" title="Mathematical logic">Mathematical logic</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">General</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Axiom" title="Axiom">Axiom</a>
<ul><li><a href="List_of_axioms" title="List of axioms">list</a></li></ul></li>
<li><a href="Cardinality" title="Cardinality">Cardinality</a></li>
<li><a href="First-order_logic" title="First-order logic">First-order logic</a></li>
<li><a href="Formal_proof" title="Formal proof">Formal proof</a></li>
<li><a href="Formal_semantics_(logic)" class="mw-redirect" title="Formal semantics (logic)">Formal semantics</a></li>
<li><a href="Foundations_of_mathematics" title="Foundations of mathematics">Foundations of mathematics</a></li>
<li><a href="Information_theory" title="Information theory">Information theory</a></li>
<li><a href="Lemma_(mathematics)" title="Lemma (mathematics)">Lemma</a></li>
<li><a href="Logical_consequence" title="Logical consequence">Logical consequence</a></li>
<li><a href="Structure_(mathematical_logic)" title="Structure (mathematical logic)">Model</a></li>
<li><a href="Theorem" title="Theorem">Theorem</a></li>
<li><a href="Theory_(mathematical_logic)" title="Theory (mathematical logic)">Theory</a></li>
<li><a href="Type_theory" title="Type theory">Type theory</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Theorems (list)<br> and <a href="Paradoxes_of_set_theory" title="Paradoxes of set theory">paradoxes</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="G%C3%B6del's_completeness_theorem" title="Gödel's completeness theorem">Gödel's completeness</a> and <a href="G%C3%B6del's_incompleteness_theorems" title="Gödel's incompleteness theorems">incompleteness theorems</a></li>
<li><a href="Tarski's_undefinability_theorem" title="Tarski's undefinability theorem">Tarski's undefinability</a></li>
<li><a href="Banach%E2%80%93Tarski_paradox" title="Banach–Tarski paradox">Banach–Tarski paradox</a></li>
<li>Cantor's <a href="Cantor's_theorem" title="Cantor's theorem">theorem,</a> <a href="Cantor's_paradox" title="Cantor's paradox">paradox</a> and <a href="Cantor's_diagonal_argument" title="Cantor's diagonal argument">diagonal argument</a></li>
<li><a href="Compactness_theorem" title="Compactness theorem">Compactness</a></li>
<li><a href="Halting_problem" title="Halting problem">Halting problem</a></li>
<li><a href="Lindstr%C3%B6m's_theorem" title="Lindström's theorem">Lindström's</a></li>
<li><a href="L%C3%B6wenheim%E2%80%93Skolem_theorem" title="Löwenheim–Skolem theorem">Löwenheim–Skolem</a></li>
<li><a href="Russell's_paradox" title="Russell's paradox">Russell's paradox</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Logic" title="Logic">Logics</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th id="Traditional95" scope="row" class="navbox-group" style="width:1%"><a href="Term_logic" title="Term logic">Traditional</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Classical_logic" title="Classical logic">Classical logic</a></li>
<li><a href="Logical_truth" title="Logical truth">Logical truth</a></li>
<li><a href="Tautology_(logic)" title="Tautology (logic)">Tautology</a></li>
<li><a href="Proposition" title="Proposition">Proposition</a></li>
<li><a href="Inference" title="Inference">Inference</a></li>
<li><a href="Logical_equivalence" title="Logical equivalence">Logical equivalence</a></li>
<li><a href="Consistency" title="Consistency">Consistency</a>
<ul><li><a href="Equiconsistency" title="Equiconsistency">Equiconsistency</a></li></ul></li>
<li><a href="Argument" title="Argument">Argument</a></li>
<li><a href="Soundness" title="Soundness">Soundness</a></li>
<li><a href="Validity_(logic)" title="Validity (logic)">Validity</a></li>
<li><a href="Syllogism" title="Syllogism">Syllogism</a></li>
<li><a href="Square_of_opposition" title="Square of opposition">Square of opposition</a></li>
<li><a href="Venn_diagram" title="Venn diagram">Venn diagram</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">Propositional</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Boolean_algebra" title="Boolean algebra">Boolean algebra</a></li>
<li><a href="Boolean_function" title="Boolean function">Boolean functions</a></li>
<li><a href="Logical_connective" title="Logical connective">Logical connectives</a></li>
<li><a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">Propositional calculus</a></li>
<li><a href="Propositional_formula" title="Propositional formula">Propositional formula</a></li>
<li><a href="Truth_table" title="Truth table">Truth tables</a></li>
<li><a href="Many-valued_logic" title="Many-valued logic">Many-valued logic</a>
<ul><li><a href="Three-valued_logic" title="Three-valued logic">3</a></li>
<li><a href="Finite-valued_logic" title="Finite-valued logic">finite</a></li>
<li><a href="Infinite-valued_logic" title="Infinite-valued logic">∞</a></li></ul></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Predicate_logic" class="mw-redirect" title="Predicate logic">Predicate</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="First-order_logic" title="First-order logic">First-order</a>
<ul><li><a href="List_of_first-order_theories" title="List of first-order theories"><span style="font-size: 85%;">list</span></a></li></ul></li>
<li><a href="Second-order_logic" title="Second-order logic">Second-order</a>
<ul><li><a href="Monadic_second-order_logic" title="Monadic second-order logic">Monadic</a></li></ul></li>
<li><a href="Higher-order_logic" title="Higher-order logic">Higher-order</a></li>
<li><a href="Fixed-point_logic" title="Fixed-point logic">Fixed-point</a></li>
<li><a href="Free_logic" title="Free logic">Free</a></li>
<li><a href="Quantifier_(logic)" title="Quantifier (logic)">Quantifiers</a></li>
<li><a href="Predicate_(mathematical_logic)" class="mw-redirect" title="Predicate (mathematical logic)">Predicate</a></li>
<li><a href="Monadic_predicate_calculus" title="Monadic predicate calculus">Monadic predicate calculus</a></li></ul>
</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Set_theory" title="Set theory">Set theory</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><td colspan="2" class="navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Zermelo%E2%80%93Fraenkel_set_theory" title="Zermelo–Fraenkel set theory">Set</a>
<ul><li><a href="Hereditary_set" title="Hereditary set">hereditary</a></li></ul></li>
<li><a href="Class_(set_theory)" title="Class (set theory)">Class</a></li>
<li>(<a href="Urelement" title="Urelement">Ur-</a>)<a href="Element_(mathematics)" title="Element (mathematics)">Element</a></li>
<li><a href="Ordinal_number" title="Ordinal number">Ordinal number</a></li>
<li><a href="Extensionality" title="Extensionality">Extensionality</a></li>
<li><a href="Forcing_(mathematics)" title="Forcing (mathematics)">Forcing</a></li>
<li><a href="Relation_(mathematics)" title="Relation (mathematics)">Relation</a>
<ul><li><a href="Equivalence_relation" title="Equivalence relation">equivalence</a></li>
<li><a href="Partition_of_a_set" title="Partition of a set">partition</a></li></ul></li>
<li>Set operations:
<ul><li><a href="Intersection_(set_theory)" title="Intersection (set theory)">intersection</a></li>
<li><a href="Union_(set_theory)" title="Union (set theory)">union</a></li>
<li><a href="Complement_(set_theory)" title="Complement (set theory)">complement</a></li>
<li><a href="Cartesian_product" title="Cartesian product">Cartesian product</a></li>
<li><a href="Power_set" title="Power set">power set</a></li>
<li><a href="List_of_set_identities_and_relations" title="List of set identities and relations">identities</a></li></ul></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Types of <a href="Set_(mathematics)" title="Set (mathematics)">sets</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Countable_set" title="Countable set">Countable</a></li>
<li><a href="Uncountable_set" title="Uncountable set">Uncountable</a></li>
<li><a href="Empty_set" title="Empty set">Empty</a></li>
<li><a href="Inhabited_set" title="Inhabited set">Inhabited</a></li>
<li><a href="Singleton_(mathematics)" title="Singleton (mathematics)">Singleton</a></li>
<li><a href="Finite_set" title="Finite set">Finite</a></li>
<li><a href="Infinite_set" title="Infinite set">Infinite</a></li>
<li><a href="Transitive_set" title="Transitive set">Transitive</a></li>
<li><a href="Ultrafilter_(set_theory)" class="mw-redirect" title="Ultrafilter (set theory)">Ultrafilter</a></li>
<li><a href="Recursive_set" class="mw-redirect" title="Recursive set">Recursive</a></li>
<li><a href="Fuzzy_set" title="Fuzzy set">Fuzzy</a></li>
<li><a href="Universal_set" title="Universal set">Universal</a></li>
<li><a href="Universe_(mathematics)" title="Universe (mathematics)">Universe</a>
<ul><li><a href="Constructible_universe" title="Constructible universe">constructible</a></li>
<li><a href="Grothendieck_universe" title="Grothendieck universe">Grothendieck</a></li>
<li><a href="Von_Neumann_universe" title="Von Neumann universe">Von Neumann</a></li></ul></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Map_(mathematics)" title="Map (mathematics)">Maps</a> and <a href="Cardinality" title="Cardinality">cardinality</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Function_(mathematics)" title="Function (mathematics)">Function</a>/<a href="Map_(mathematics)" title="Map (mathematics)">Map</a>
<ul><li><a href="Domain_of_a_function" title="Domain of a function">domain</a></li>
<li><a href="Codomain" title="Codomain">codomain</a></li>
<li><a href="Image_(mathematics)" title="Image (mathematics)">image</a></li></ul></li>
<li><a href="Injective_function" title="Injective function">In</a>/<a href="Surjective_function" title="Surjective function">Sur</a>/<a href="Bijection" title="Bijection">Bi</a>-jection</li>
<li><a href="Schr%C3%B6der%E2%80%93Bernstein_theorem" title="Schröder–Bernstein theorem">Schröder–Bernstein theorem</a></li>
<li><a href="Isomorphism" title="Isomorphism">Isomorphism</a></li>
<li><a href="G%C3%B6del_numbering" title="Gödel numbering">Gödel numbering</a></li>
<li><a href="Enumeration" title="Enumeration">Enumeration</a></li>
<li><a href="Large_cardinal" title="Large cardinal">Large cardinal</a>
<ul><li><a href="Inaccessible_cardinal" title="Inaccessible cardinal">inaccessible</a></li></ul></li>
<li><a href="Aleph_number" title="Aleph number">Aleph number</a></li>
<li><a href="Operation_(mathematics)" title="Operation (mathematics)">Operation</a>
<ul><li><a href="Binary_operation" title="Binary operation">binary</a></li></ul></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Set theories</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Zermelo%E2%80%93Fraenkel_set_theory" title="Zermelo–Fraenkel set theory">Zermelo–Fraenkel</a>
<ul><li><a href="Axiom_of_choice" title="Axiom of choice">axiom of choice</a></li>
<li><a href="Continuum_hypothesis" title="Continuum hypothesis">continuum hypothesis</a></li></ul></li>
<li><a href="General_set_theory" title="General set theory">General</a></li>
<li><a href="Kripke%E2%80%93Platek_set_theory" title="Kripke–Platek set theory">Kripke–Platek</a></li>
<li><a href="Morse%E2%80%93Kelley_set_theory" title="Morse–Kelley set theory">Morse–Kelley</a></li>
<li><a href="Naive_set_theory" title="Naive set theory">Naive</a></li>
<li><a href="New_Foundations" title="New Foundations">New Foundations</a></li>
<li><a href="Tarski%E2%80%93Grothendieck_set_theory" title="Tarski–Grothendieck set theory">Tarski–Grothendieck</a></li>
<li><a href="Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory" title="Von Neumann–Bernays–Gödel set theory">Von Neumann–Bernays–Gödel</a></li>
<li><a href="Ackermann_set_theory" title="Ackermann set theory">Ackermann</a></li>
<li><a href="Constructive_set_theory" title="Constructive set theory">Constructive</a></li></ul>
</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Formal_system" title="Formal system">Formal systems</a> (<a href="List_of_formal_systems" title="List of formal systems"><span style="font-size: 85%;">list</span></a>),<br> and <a href="Syntax_(logic)" title="Syntax (logic)">syntax</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><td colspan="2" class="navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Alphabet_(formal_languages)" title="Alphabet (formal languages)">Alphabet</a></li>
<li><a href="Arity" title="Arity">Arity</a></li>
<li><a href="Automata_theory" title="Automata theory">Automata</a></li>
<li><a href="Axiom_schema" title="Axiom schema">Axiom schema</a></li>
<li><a href="Expression_(mathematics)" title="Expression (mathematics)">Expression</a>
<ul><li><a href="Ground_expression" title="Ground expression">ground</a></li></ul></li>
<li><a href="Extension_by_new_constant_and_function_names" title="Extension by new constant and function names">Extension</a>
<ul><li><a href="Extension_by_definitions" class="mw-redirect" title="Extension by definitions">by definition</a></li>
<li><a href="Conservative_extension" title="Conservative extension">conservative</a></li></ul></li>
<li><a href="Finitary_relation" title="Finitary relation">Relation</a></li>
<li><a href="Formation_rule" title="Formation rule">Formation rule</a></li>
<li><a href="Formal_grammar" title="Formal grammar">Grammar</a></li>
<li><a href="Well-formed_formula" title="Well-formed formula">Formula</a>
<ul><li><a href="Atomic_formula" title="Atomic formula">atomic</a></li>
<li><a href="Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">closed</a></li>
<li><a href="Ground_formula" class="mw-redirect" title="Ground formula">ground</a></li>
<li><a href="Open_formula" title="Open formula">open</a></li></ul></li>
<li><a href="Free_variables_and_bound_variables" title="Free variables and bound variables">Free/bound variable</a></li>
<li><a href="Metalanguage" title="Metalanguage">Metalanguage</a></li>
<li><a href="Logical_connective" title="Logical connective">Logical connective</a>
<ul><li><a href="Negation" title="Negation">¬</a></li>
<li><a href="Logical_disjunction" title="Logical disjunction">∨</a></li>
<li><a href="Logical_conjunction" title="Logical conjunction">∧</a></li>
<li><a href="Material_conditional" title="Material conditional">→</a></li>
<li><a href="Logical_biconditional" title="Logical biconditional">↔</a></li>
<li><a href="Logical_equality" title="Logical equality">=</a></li></ul></li>
<li><a href="Predicate_(mathematical_logic)" class="mw-redirect" title="Predicate (mathematical logic)">Predicate</a>
<ul><li><a href="Functional_predicate" title="Functional predicate">functional</a></li>
<li><a href="Predicate_variable" title="Predicate variable">variable</a></li>
<li><a href="Propositional_variable" title="Propositional variable">propositional variable</a></li></ul></li>
<li><a href="Formal_proof" title="Formal proof">Proof</a></li>
<li><a href="Quantifier_(logic)" title="Quantifier (logic)">Quantifier</a>
<ul><li><a href="Existential_quantification" title="Existential quantification">∃</a></li>
<li><a href="Uniqueness_quantification" title="Uniqueness quantification">!</a></li>
<li><a href="Universal_quantification" title="Universal quantification">∀</a></li>
<li><a href="Quantifier_rank" title="Quantifier rank">rank</a></li></ul></li>
<li><a href="Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">Sentence</a>
<ul><li><a href="Atomic_sentence" title="Atomic sentence">atomic</a></li>
<li><a href="Spectrum_of_a_sentence" title="Spectrum of a sentence">spectrum</a></li></ul></li>
<li><a href="Signature_(logic)" title="Signature (logic)">Signature</a></li>
<li><a href="String_(formal_languages)" class="mw-redirect" title="String (formal languages)">String</a></li>
<li><a href="Substitution_(logic)" title="Substitution (logic)">Substitution</a></li>
<li><a href="Symbol_(formal)" title="Symbol (formal)">Symbol</a>
<ul><li><a href="Uninterpreted_function" title="Uninterpreted function">function</a></li>
<li><a href="Logical_constant" title="Logical constant">logical/constant</a></li>
<li><a href="Non-logical_symbol" title="Non-logical symbol">non-logical</a></li>
<li><a href="Variable_(mathematics)" title="Variable (mathematics)">variable</a></li></ul></li>
<li><a href="Term_(logic)" title="Term (logic)">Term</a></li>
<li><a href="Theory_(mathematical_logic)" title="Theory (mathematical logic)">Theory</a>
<ul><li><a href="List_of_mathematical_theories" title="List of mathematical theories"><span style="font-size: 85%;">list</span></a></li></ul></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><span class="nowrap">Example <a href="Axiomatic_system" title="Axiomatic system">axiomatic<br>systems</a> <span style="font-size: 85%;">(<a href="List_of_first-order_theories" title="List of first-order theories">list</a>)</span></span></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li>of <a href="True_arithmetic" title="True arithmetic">arithmetic</a>:
<ul><li><a href="Peano_axioms" title="Peano axioms">Peano</a></li>
<li><a href="Second-order_arithmetic" title="Second-order arithmetic">second-order</a></li>
<li><a href="Elementary_function_arithmetic" title="Elementary function arithmetic">elementary function</a></li>
<li><a href="Primitive_recursive_arithmetic" title="Primitive recursive arithmetic">primitive recursive</a></li>
<li><a href="Robinson_arithmetic" title="Robinson arithmetic">Robinson</a></li>
<li><a href="Skolem_arithmetic" title="Skolem arithmetic">Skolem</a></li></ul></li>
<li>of the <a href="Construction_of_the_real_numbers" title="Construction of the real numbers">real numbers</a>
<ul><li><a href="Tarski's_axiomatization_of_the_reals" title="Tarski's axiomatization of the reals">Tarski's axiomatization</a></li></ul></li>
<li>of <a href="Axiomatization_of_Boolean_algebras" class="mw-redirect" title="Axiomatization of Boolean algebras">Boolean algebras</a>
<ul><li><a href="Boolean_algebras_canonically_defined" title="Boolean algebras canonically defined">canonical</a></li>
<li><a href="Minimal_axioms_for_Boolean_algebra" title="Minimal axioms for Boolean algebra">minimal axioms</a></li></ul></li>
<li>of <a href="Foundations_of_geometry" title="Foundations of geometry">geometry</a>:
<ul><li><a href="Euclidean_geometry" title="Euclidean geometry">Euclidean</a>:
<ul><li><a href="Euclid's_Elements" title="Euclid's Elements"><i>Elements</i></a></li>
<li><a href="Hilbert's_axioms" title="Hilbert's axioms">Hilbert's</a></li>
<li><a href="Tarski's_axioms" title="Tarski's axioms">Tarski's</a></li></ul></li>
<li><a href="Non-Euclidean_geometry" title="Non-Euclidean geometry">non-Euclidean</a></li></ul></li></ul>
<ul><li><i><a href="Principia_Mathematica" title="Principia Mathematica">Principia Mathematica</a></i></li></ul>
</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Proof_theory" title="Proof theory">Proof theory</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Formal_proof" title="Formal proof">Formal proof</a></li>
<li><a href="Natural_deduction" title="Natural deduction">Natural deduction</a></li>
<li><a href="Logical_consequence" title="Logical consequence">Logical consequence</a></li>
<li><a href="Rule_of_inference" title="Rule of inference">Rule of inference</a></li>
<li><a href="Sequent_calculus" title="Sequent calculus">Sequent calculus</a></li>
<li><a href="Theorem" title="Theorem">Theorem</a></li>
<li><a href="Formal_system" title="Formal system">Systems</a>
<ul><li><a href="Axiomatic_system" title="Axiomatic system">axiomatic</a></li>
<li><a href="Deductive_system" class="mw-redirect" title="Deductive system">deductive</a></li>
<li><a href="Hilbert_system" title="Hilbert system">Hilbert</a>
<ul><li><a href="List_of_Hilbert_systems" class="mw-redirect" title="List of Hilbert systems">list</a></li></ul></li></ul></li>
<li><a href="Complete_theory" title="Complete theory">Complete theory</a></li>
<li><a href="Independence_(mathematical_logic)" title="Independence (mathematical logic)">Independence</a> (<a href="List_of_statements_independent_of_ZFC" title="List of statements independent of ZFC">from ZFC</a>)</li>
<li><a href="Proof_of_impossibility" title="Proof of impossibility">Proof of impossibility</a></li>
<li><a href="Ordinal_analysis" title="Ordinal analysis">Ordinal analysis</a></li>
<li><a href="Reverse_mathematics" title="Reverse mathematics">Reverse mathematics</a></li>
<li><a href="Self-verifying_theories" title="Self-verifying theories">Self-verifying theories</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Model_theory" title="Model theory">Model theory</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Interpretation_(logic)" title="Interpretation (logic)">Interpretation</a>
<ul><li><a href="Interpretation_function" class="mw-redirect" title="Interpretation function">function</a></li>
<li><a href="Interpretation_(model_theory)" title="Interpretation (model theory)">of models</a></li></ul></li>
<li><a href="Structure_(mathematical_logic)" title="Structure (mathematical logic)">Model</a>
<ul><li><a href="Elementary_equivalence" title="Elementary equivalence">equivalence</a></li>
<li><a href="Finite_model_theory" title="Finite model theory">finite</a></li>
<li><a href="Saturated_model" title="Saturated model">saturated</a></li>
<li><a href="Spectrum_of_a_theory" title="Spectrum of a theory">spectrum</a></li>
<li><a href="Substructure_(mathematics)" title="Substructure (mathematics)">submodel</a></li></ul></li>
<li><a href="Non-standard_model" title="Non-standard model">Non-standard model</a>
<ul><li><a href="Non-standard_model_of_arithmetic" title="Non-standard model of arithmetic">of arithmetic</a></li></ul></li>
<li><a href="Diagram_(mathematical_logic)" title="Diagram (mathematical logic)">Diagram</a>
<ul><li><a href="Elementary_diagram" title="Elementary diagram">elementary</a></li></ul></li>
<li><a href="Categorical_theory" title="Categorical theory">Categorical theory</a></li>
<li><a href="Model_complete_theory" title="Model complete theory">Model complete theory</a></li>
<li><a href="Satisfiability" title="Satisfiability">Satisfiability</a></li>
<li><a href="Semantics_of_logic" title="Semantics of logic">Semantics of logic</a></li>
<li><a href="Strength_(mathematical_logic)" title="Strength (mathematical logic)">Strength</a></li>
<li><a href="Theories_of_truth" class="mw-redirect" title="Theories of truth">Theories of truth</a>
<ul><li><a href="Semantic_theory_of_truth" title="Semantic theory of truth">semantic</a></li>
<li><a href="Tarski's_theory_of_truth" class="mw-redirect" title="Tarski's theory of truth">Tarski's</a></li>
<li><a href="Kripke's_theory_of_truth" class="mw-redirect" title="Kripke's theory of truth">Kripke's</a></li></ul></li>
<li><a href="T-schema" title="T-schema">T-schema</a></li>
<li><a href="Transfer_principle" title="Transfer principle">Transfer principle</a></li>
<li><a href="Truth_predicate" title="Truth predicate">Truth predicate</a></li>
<li><a href="Truth_value" title="Truth value">Truth value</a></li>
<li><a href="Type_(model_theory)" title="Type (model theory)">Type</a></li>
<li><a href="Ultraproduct" title="Ultraproduct">Ultraproduct</a></li>
<li><a href="Validity_(logic)" title="Validity (logic)">Validity</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Computability_theory" title="Computability theory">Computability theory</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Church_encoding" title="Church encoding">Church encoding</a></li>
<li><a href="Church%E2%80%93Turing_thesis" title="Church–Turing thesis">Church–Turing thesis</a></li>
<li><a href="Computably_enumerable_set" title="Computably enumerable set">Computably enumerable</a></li>
<li><a href="Computable_function" title="Computable function">Computable function</a></li>
<li><a href="Computable_set" title="Computable set">Computable set</a></li>
<li><a href="Decision_problem" title="Decision problem">Decision problem</a>
<ul><li><a href="Decidability_(logic)" title="Decidability (logic)">decidable</a></li>
<li><a href="Undecidable_problem" title="Undecidable problem">undecidable</a></li>
<li><a href="P_(complexity)" title="P (complexity)">P</a></li>
<li><a href="NP_(complexity)" title="NP (complexity)">NP</a></li>
<li><a href="P_versus_NP_problem" title="P versus NP problem">P versus NP problem</a></li></ul></li>
<li><a href="Kolmogorov_complexity" title="Kolmogorov complexity">Kolmogorov complexity</a></li>
<li><a href="Lambda_calculus" title="Lambda calculus">Lambda calculus</a></li>
<li><a href="Primitive_recursive_function" title="Primitive recursive function">Primitive recursive function</a></li>
<li><a href="Recursion" title="Recursion">Recursion</a></li>
<li><a href="Recursive_set" class="mw-redirect" title="Recursive set">Recursive set</a></li>
<li><a href="Turing_machine" title="Turing machine">Turing machine</a></li>
<li><a href="Type_theory" title="Type theory">Type theory</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Related</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Abstract_logic" title="Abstract logic">Abstract logic</a></li>
<li><a href="Algebraic_logic" title="Algebraic logic">Algebraic logic</a></li>
<li><a href="Automated_theorem_proving" title="Automated theorem proving">Automated theorem proving</a></li>
<li><a href="Category_theory" title="Category theory">Category theory</a></li>
<li><a href="Concrete_category" title="Concrete category">Concrete</a>/<a href="Category_(mathematics)" title="Category (mathematics)">Abstract category</a></li>
<li><a href="Category_of_sets" title="Category of sets">Category of sets</a></li>
<li><a href="History_of_logic" title="History of logic">History of logic</a></li>
<li><a href="History_of_mathematical_logic" class="mw-redirect" title="History of mathematical logic">History of mathematical logic</a>
<ul><li><a href="Timeline_of_mathematical_logic" title="Timeline of mathematical logic">timeline</a></li></ul></li>
<li><a href="Logicism" title="Logicism">Logicism</a></li>
<li><a href="Mathematical_object" title="Mathematical object">Mathematical object</a></li>
<li><a href="Philosophy_of_mathematics" title="Philosophy of mathematics">Philosophy of mathematics</a></li>
<li><a href="Supertask" title="Supertask">Supertask</a></li></ul>
</div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><b><span class="nowrap"><span class="skin-invert-image noviewer" typeof="mw:File"></span> </span><a href="Portal%3AMathematics" title="Portal:Mathematics">Mathematics portal</a></b></div></td></tr></tbody></table></div>
<div class="navbox-styles"><style data-mw-deduplicate="TemplateStyles:r1038841319">
/* start https://en.wikipedia.org/ */
.mw-parser-output .tooltip-dotted{border-bottom:1px dotted;cursor:help}
/* end https://en.wikipedia.org/ */
</style></div><div role="navigation" class="navbox authority-control" aria-labelledby="Authority_control_databases_frameless&#124;text-top&#124;10px&#124;alt=Edit_this_at_Wikidata&#124;link=https&#58;//www.wikidata.org/wiki/Q192161#identifiers&#124;class=noprint&#124;Edit_this_at_Wikidata1560" style="padding:3px"><table class="nowraplinks hlist mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><div id="Authority_control_databases_frameless&#124;text-top&#124;10px&#124;alt=Edit_this_at_Wikidata&#124;link=https&#58;//www.wikidata.org/wiki/Q192161#identifiers&#124;class=noprint&#124;Edit_this_at_Wikidata1560" style="font-size:114%;margin:0 4em">Authority control databases </div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">National</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"><ul><li><span class="uid"><a rel="nofollow" class="external text" href="https://d-nb.info/gnd/4017848-1">Germany</a></span></li><li><span class="uid"><a rel="nofollow" class="external text" href="https://id.loc.gov/authorities/sh85050802">United States</a></span></li><li><span class="uid"><span class="rt-commentedText tooltip tooltip-dotted" title="Langages formels"><a rel="nofollow" class="external text" href="https://catalogue.bnf.fr/ark:/12148/cb11967270h">France</a></span></span></li><li><span class="uid"><span class="rt-commentedText tooltip tooltip-dotted" title="Langages formels"><a rel="nofollow" class="external text" href="https://data.bnf.fr/ark:/12148/cb11967270h">BnF data</a></span></span></li><li><span class="uid"><a rel="nofollow" class="external text" href="https://id.ndl.go.jp/auth/ndlna/00576869">Japan</a></span></li><li><span class="uid"><span class="rt-commentedText tooltip tooltip-dotted" title="formální jazyky"><a rel="nofollow" class="external text" href="https://aleph.nkp.cz/F/?func=find-c&local_base=aut&ccl_term=ica=ph208851&CON_LNG=ENG">Czech Republic</a></span></span></li><li><span class="uid"><a rel="nofollow" class="external text" href="https://www.nli.org.il/en/authorities/987007545721205171">Israel</a></span></li></ul></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"><ul><li><span class="uid"><a rel="nofollow" class="external text" href="https://lux.collections.yale.edu/view/concept/24fceff3-ba07-48b4-a446-7f8b073ec11f">Yale LUX</a></span></li></ul></div></td></tr></tbody></table></div></div><!--htdig_noindex--><div><div class="zim-footer">
This article is issued from <a class="external text" title="Last edited on 2025-07-19" href="https://en.wikipedia.org/wiki/?title=Formal_language&oldid=1301445169">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.
</div>
</div><!--/htdig_noindex--></div>
</div>
</main>
</div>
</div>
</div>
</body></html>